src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Nov 19 18:34:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Nov 19 18:38:25 2013 +0100
@@ -17,7 +17,7 @@
 signature SLEDGEHAMMER_ANNOTATE =
 sig
   val annotate_types : Proof.context -> term -> term
-end
+end;
 
 structure Sledgehammer_Annotate : SLEDGEHAMMER_ANNOTATE =
 struct
@@ -215,4 +215,4 @@
          |> sort int_ord
   in introduce_annotations subst typing_spots t t' end
 
-end
+end;