src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML

 sig
   type isar_proof = Sledgehammer_Proof.isar_proof
   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
 
 open Sledgehammer_Util

 
   in
     do_proof proof
   end
 
-
-end
+end;