src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML

     overall_preplay_stats : isar_proof -> preplay_time * bool }
 
   val proof_preplay_interface :
     bool -> Proof.context -> string -> string -> bool -> Time.time
     -> isar_proof -> preplay_interface
-end
+end;
 
 structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
 struct
 
 open Sledgehammer_Util

         set_preplay_time = set_preplay_time,
         preplay_quietly = preplay_quietly,
         overall_preplay_stats = overall_preplay_stats}
     end
 
-end
+end;