--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Mon Jun 02 17:34:26 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Mon Jun 02 17:34:27 2014 +0200
@@ -158,8 +158,7 @@
reraise exn
else
{outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
- rewrite_rules = [], conjecture_id = ~1, prem_ids = [], helper_ids = [],
- fact_ids = [], z3_proof = []}
+ fact_ids = [], atp_proof = K []}
val death = Timer.checkRealTimer timer
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
@@ -226,8 +225,7 @@
end
val weighted_factss = map (apsnd weight_facts) factss
- val {outcome, filter_result = {rewrite_rules, conjecture_id, prem_ids, helper_ids, fact_ids,
- z3_proof, ...}, used_from, run_time} =
+ val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
smt2_filter_loop name params state goal subgoal weighted_factss
val used_named_facts = map snd fact_ids
val used_facts = map fst used_named_facts
@@ -242,20 +240,8 @@
fn preplay =>
let
fun isar_params () =
- let
- val fact_helper_ts =
- map (fn (_, th) => (short_thm_name ctxt th, prop_of th)) helper_ids @
- map (fn ((s, _), th) => (s, prop_of th)) used_named_facts
- val fact_helper_ids =
- map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
- map (fn (id, ((name, _), _)) => (id, name)) fact_ids
-
- val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts
- concl_t fact_helper_ts prem_ids conjecture_id fact_helper_ids z3_proof
- in
- (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
- minimize <> SOME false, atp_proof, goal)
- end
+ (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
+ minimize <> SOME false, atp_proof (), goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,