# HG changeset patch
# User blanchet
# Date 1384882705 -3600
# Node ID 096f7d45216479a300afd98f63978ce84e2f605c
# Parent  b490e15a5e19b41b8b45751edc5b9f92140e9e56
tuning

diff -r b490e15a5e19 -r 096f7d452164 src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Nov 19 18:34:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Nov 19 18:38:25 2013 +0100
@@ -17,7 +17,7 @@
 signature SLEDGEHAMMER_ANNOTATE =
 sig
   val annotate_types : Proof.context -> term -> term
-end
+end;
 
 structure Sledgehammer_Annotate : SLEDGEHAMMER_ANNOTATE =
 struct
@@ -215,4 +215,4 @@
          |> sort int_ord
   in introduce_annotations subst typing_spots t t' end
 
-end
+end;
diff -r b490e15a5e19 -r 096f7d452164 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;
diff -r b490e15a5e19 -r 096f7d452164 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Tue Nov 19 18:34:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Tue Nov 19 18:38:25 2013 +0100
@@ -11,7 +11,7 @@
   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
@@ -105,4 +105,4 @@
     snd (do_proof proof)
   end
 
-end
+end;
diff -r b490e15a5e19 -r 096f7d452164 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Tue Nov 19 18:34:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Tue Nov 19 18:38:25 2013 +0100
@@ -35,7 +35,7 @@
   val proof_preplay_interface :
     bool -> Proof.context -> string -> string -> bool -> Time.time
     -> isar_proof -> preplay_interface
-end
+end;
 
 structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
 struct
@@ -312,4 +312,4 @@
         overall_preplay_stats = overall_preplay_stats}
     end
 
-end
+end;
diff -r b490e15a5e19 -r 096f7d452164 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Tue Nov 19 18:34:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Tue Nov 19 18:38:25 2013 +0100
@@ -293,4 +293,4 @@
             of_indent 0 ^ (if n <> 1 then "next" else "qed")
   end
 
-end
+end;
diff -r b490e15a5e19 -r 096f7d452164 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Tue Nov 19 18:34:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Tue Nov 19 18:38:25 2013 +0100
@@ -67,7 +67,7 @@
 
   structure Canonical_Lbl_Tab : TABLE
 
-end
+end;
 
 structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
 struct
@@ -196,4 +196,4 @@
     fst (do_proof proof (0, []))
   end
 
-end
+end;
diff -r b490e15a5e19 -r 096f7d452164 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
--- 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;