--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Wed Jul 30 23:52:56 2014 +0200
@@ -196,10 +196,12 @@
(case outcome of
NONE =>
(Lazy.lazy (fn () =>
- play_one_line_proof mode verbose preplay_timeout used_named_facts state subgoal
- SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+ play_one_line_proof mode preplay_timeout used_named_facts state subgoal SMT2_Method
+ (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
+ val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+
fun isar_params () =
(verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
goal)