# HG changeset patch
# User blanchet
# Date 1366727430 -7200
# Node ID 3fc8eb5c0915b79bb49b84517f8a77da1fc92f1a
# Parent  97c116445b652b933e2b8fbdcc9d8e19d0e07887
tuning

diff -r 97c116445b65 -r 3fc8eb5c0915 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Tue Apr 23 16:30:29 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Tue Apr 23 16:30:30 2013 +0200
@@ -9,7 +9,7 @@
 sig
   type isar_proof = Sledgehammer_Proof.isar_proof
   type preplay_time = Sledgehammer_Preplay.preplay_time
-  val compress_proof :
+  val compress_and_preplay_proof :
     bool -> Proof.context -> string -> string -> bool -> Time.time option
     -> real -> isar_proof -> isar_proof * (bool * preplay_time)
 end
@@ -46,8 +46,8 @@
 fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
 
 (* Main function for compresing proofs *)
-fun compress_proof debug ctxt type_enc lam_trans preplay preplay_timeout
-                   isar_compress proof =
+fun compress_and_preplay_proof debug ctxt type_enc lam_trans preplay
+                               preplay_timeout isar_compress proof =
   let
     (* 60 seconds seems like a good interpreation of "no timeout" *)
     val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
diff -r 97c116445b65 -r 3fc8eb5c0915 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Apr 23 16:30:29 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Apr 23 16:30:30 2013 +0200
@@ -445,7 +445,7 @@
       else if nr=1 orelse member (op=) qs Then
         then of_thus_hence qs
         else of_show_have qs
-    fun add_term term (s, ctxt)=
+    fun add_term term (s, ctxt) =
       (s ^ (annotate_types ctxt term
             |> with_vanilla_print_mode (Syntax.string_of_term ctxt)
             |> simplify_spaces
@@ -780,7 +780,7 @@
             do_proof true params assms infs
           end
 
-        val cleanup_labels_in_proof =
+        val clean_up_labels_in_proof =
           chain_direct_proof
           #> kill_useless_labels_in_proof
           #> relabel_proof
@@ -791,10 +791,10 @@
           |> (if not preplay andalso isar_compress <= 1.0 then
                 rpair (false, (true, seconds 0.0))
               else
-                compress_proof debug ctxt type_enc lam_trans preplay
+                compress_and_preplay_proof debug ctxt type_enc lam_trans preplay
                   preplay_timeout
                   (if isar_proofs = SOME true then isar_compress else 1000.0))
-          |>> cleanup_labels_in_proof
+          |>> clean_up_labels_in_proof
         val isar_text =
           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
                            isar_proof
@@ -820,8 +820,8 @@
                else
                  [])
           in
-            "\n\nStructured proof "
-              ^ (commas msg |> not (null msg) ? enclose "(" ")")
+            "\n\nStructured proof"
+              ^ (commas msg |> not (null msg) ? enclose " (" ")")
               ^ ":\n" ^ Active.sendback_markup isar_text
           end
       end
diff -r 97c116445b65 -r 3fc8eb5c0915 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Apr 23 16:30:29 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Apr 23 16:30:30 2013 +0200
@@ -276,7 +276,7 @@
         if null smts then accum else launch_provers state "SMT solver" NONE smts
       val launch_full_atps = launch_atps "ATP" NONE full_atps
       val launch_ueq_atps =
-        launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps
+        launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps
       fun launch_atps_and_smt_solvers () =
         [launch_full_atps, launch_smts, launch_ueq_atps]
         |> Par_List.map (fn f => ignore (f (unknownN, state)))