diff -r 6dc80eead659 -r 0b430064296a src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed Nov 28 12:25:43 2012 +0100
@@ -1,3 +1,11 @@
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Steffen Juilf Smolka, TU Muenchen
+
+Supplement term with explicit type constraints that show up as 
+type annotations when printing the term.
+*)
+
 signature SLEDGEHAMMER_ANNOTATE =
 sig
   val annotate_types : Proof.context -> term -> term