1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 13 13:18:14 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 13 13:18:14 2014 +0100
     1.3 @@ -112,7 +112,7 @@
     1.4    * (term, string) atp_step list * thm
     1.5  
     1.6  val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method]
     1.7 -val simp_based_methods = [Simp_Method, Auto_Method, Fastforce_Method, Force_Method]
     1.8 +val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
     1.9  val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
    1.10  
    1.11  val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
    1.12 @@ -125,6 +125,8 @@
    1.13  fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
    1.14      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
    1.15    let
    1.16 +    val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
    1.17 +
    1.18      fun isar_proof_of () =
    1.19        let
    1.20          val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
    1.21 @@ -272,8 +274,6 @@
    1.22          and isar_proof outer fix assms lems infs =
    1.23            Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
    1.24  
    1.25 -        val string_of_isar_proof = string_of_isar_proof ctxt subgoal subgoal_count
    1.26 -
    1.27          val trace = Config.get ctxt trace
    1.28  
    1.29          val canonical_isar_proof =
    1.30 @@ -303,7 +303,8 @@
    1.31          fun trace_isar_proof label proof =
    1.32            if trace then
    1.33              tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
    1.34 -              string_of_isar_proof (comment_isar_proof comment_of proof) ^ "\n")
    1.35 +              string_of_isar_proof ctxt subgoal subgoal_count
    1.36 +                (comment_isar_proof comment_of proof) ^ "\n")
    1.37            else
    1.38              ()
    1.39  
    1.40 @@ -335,7 +336,7 @@
    1.41                 #> kill_useless_labels_in_isar_proof
    1.42                 #> relabel_isar_proof_nicely)
    1.43        in
    1.44 -        (case string_of_isar_proof isar_proof of
    1.45 +        (case string_of_isar_proof ctxt subgoal subgoal_count isar_proof of
    1.46            "" =>
    1.47            if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
    1.48            else ""
    1.49 @@ -363,7 +364,7 @@
    1.50          (case try isar_proof_of () of
    1.51            SOME s => s
    1.52          | NONE =>
    1.53 -          if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
    1.54 +          if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")
    1.55    in one_line_proof ^ isar_proof end
    1.56  
    1.57  fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =