src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Tue Nov 19 18:34:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Tue Nov 19 18:38:25 2013 +0100
@@ -15,8 +15,7 @@
   type preplay_interface = Sledgehammer_Preplay.preplay_interface
 
   val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof
-end
-
+end;
 
 structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
 struct
@@ -370,5 +369,4 @@
     do_proof proof
   end
 
-
-end
+end;