src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML

 sig
   type preplay_interface = Sledgehammer_Preplay.preplay_interface
   type isar_proof = Sledgehammer_Proof.isar_proof
   val minimize_dependencies_and_remove_unrefed_steps :
     bool -> preplay_interface -> isar_proof -> isar_proof
-end
+end;
 
 structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
 struct
 
 open Sledgehammer_Util

         end
   in
     snd (do_proof proof)
   end
 
-end
+end;