# HG changeset patch
# User blanchet
# Date 1394713094 -3600
# Node ID 8e7a9ad44e14f13cc1d16508c08b82de742d9939
# Parent  3e717b56e955e88487ac2514a4c1a8f46cea2751
tuning

diff -r 3e717b56e955 -r 8e7a9ad44e14 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -112,7 +112,7 @@
   * (term, string) atp_step list * thm
 
 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method]
-val simp_based_methods = [Simp_Method, Auto_Method, Fastforce_Method, Force_Method]
+val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
 
 val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
@@ -125,6 +125,8 @@
 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
+    val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
+
     fun isar_proof_of () =
       let
         val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
@@ -272,8 +274,6 @@
         and isar_proof outer fix assms lems infs =
           Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
 
-        val string_of_isar_proof = string_of_isar_proof ctxt subgoal subgoal_count
-
         val trace = Config.get ctxt trace
 
         val canonical_isar_proof =
@@ -303,7 +303,8 @@
         fun trace_isar_proof label proof =
           if trace then
             tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
-              string_of_isar_proof (comment_isar_proof comment_of proof) ^ "\n")
+              string_of_isar_proof ctxt subgoal subgoal_count
+                (comment_isar_proof comment_of proof) ^ "\n")
           else
             ()
 
@@ -335,7 +336,7 @@
                #> kill_useless_labels_in_isar_proof
                #> relabel_isar_proof_nicely)
       in
-        (case string_of_isar_proof isar_proof of
+        (case string_of_isar_proof ctxt subgoal subgoal_count isar_proof of
           "" =>
           if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
           else ""
@@ -363,7 +364,7 @@
         (case try isar_proof_of () of
           SOME s => s
         | NONE =>
-          if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
+          if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")
   in one_line_proof ^ isar_proof end
 
 fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =