--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Tue Nov 19 18:34:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Tue Nov 19 18:38:25 2013 +0100
@@ -12,7 +12,7 @@
type preplay_interface = Sledgehammer_Preplay.preplay_interface
val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
-end
+end;
structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =
struct
@@ -59,4 +59,4 @@
fun try0 preplay_timeout preplay_interface proof =
map_isar_steps (try0_step preplay_timeout preplay_interface) proof
-end
+end;