diff --git a/src/muz/transforms/dl_mk_separate_negated_tails.cpp b/src/muz/transforms/dl_mk_separate_negated_tails.cpp
index 18e7feadf..782e1011d 100644
--- a/src/muz/transforms/dl_mk_separate_negated_tails.cpp
+++ b/src/muz/transforms/dl_mk_separate_negated_tails.cpp
@@ -1,3 +1,21 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    mk_separate_negated_tails.cpp
+
+Abstract:
+
+    <see header>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-09-09
+
+Revision History:
+
+--*/
 
 #include "dl_mk_separate_negated_tails.h"
 #include "dl_context.h"
diff --git a/src/muz/transforms/dl_mk_separate_negated_tails.h b/src/muz/transforms/dl_mk_separate_negated_tails.h
index 4b1673307..8cd806f43 100644
--- a/src/muz/transforms/dl_mk_separate_negated_tails.h
+++ b/src/muz/transforms/dl_mk_separate_negated_tails.h
@@ -1,5 +1,5 @@
 /*++
-Copyright (c) 2006 Microsoft Corporation
+Copyright (c) 2013 Microsoft Corporation
 
 Module Name:
 
@@ -21,9 +21,6 @@ Abstract:
        P(x)    :- Exists y, z . Q(x,y), !R(y,z), TN(z).
        TN(z)   :- !T(z,u).
 
-
-
-
 Author:
 
     Nikolaj Bjorner (nbjorner) 2013-09-09