--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 18 20:53:22 2013 +0200
@@ -973,7 +973,7 @@
subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
- proof_text ctxt isar_proofs isar_params num_chained
+ proof_text ctxt (mode = Auto_Try) isar_proofs isar_params num_chained
one_line_params
end,
(if verbose then
@@ -1177,7 +1177,7 @@
preplay,
subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
- in one_line_proof_text num_chained one_line_params end,
+ in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
if verbose then
"\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
else
@@ -1222,7 +1222,7 @@
minimize_command override_params name, subgoal,
subgoal_count)
val num_chained = length (#facts (Proof.goal state))
- in one_line_proof_text num_chained one_line_params end,
+ in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
message_tail = ""}
| play =>
let