--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:32:02 2014 +0100
@@ -16,11 +16,11 @@
val trace : bool Config.T
type isar_params =
- bool * (string option * string option) * Time.time * real * bool * bool * bool
+ bool * (string option * string option) * Time.time * real * bool * bool
* (term, string) atp_step list * thm
- val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
- one_line_params -> string
+ val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
+ int -> one_line_params -> string
end;
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -108,7 +108,7 @@
end
type isar_params =
- bool * (string option * string option) * Time.time * real * bool * bool * bool
+ bool * (string option * string option) * Time.time * real * bool * bool
* (term, string) atp_step list * thm
val arith_methods =
@@ -126,18 +126,18 @@
val skolem_methods =
[Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
-fun isar_proof_text ctxt debug isar_proofs isar_params
+fun isar_proof_text ctxt debug isar_proofs smt isar_params
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
fun isar_proof_of () =
let
- val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, smt, minimize,
+ val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
atp_proof, goal) = try isar_params ()
val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
fun massage_meths (meths as meth :: _) =
- if not try0_isar then [meth] else if smt then SMT_Method :: meths else meths
+ if not try0_isar then [meth] else if smt = SOME true then SMT_Method :: meths else meths
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
@@ -355,18 +355,18 @@
if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
in one_line_proof ^ isar_proof end
-fun isar_proof_would_be_a_good_idea (meth, play) =
+fun isar_proof_would_be_a_good_idea smt (meth, play) =
(case play of
- Played _ => meth = SMT_Method
+ Played _ => meth = SMT_Method andalso smt <> SOME true
| Play_Timed_Out _ => true
| Play_Failed => true
| Not_Played => false)
-fun proof_text ctxt debug isar_proofs isar_params num_chained
+fun proof_text ctxt debug isar_proofs smt isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =
(if isar_proofs = SOME true orelse
- (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
- isar_proof_text ctxt debug isar_proofs isar_params
+ (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt preplay) then
+ isar_proof_text ctxt debug isar_proofs smt isar_params
else
one_line_proof_text num_chained) one_line_params