--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri May 16 17:11:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri May 16 19:13:50 2014 +0200
@@ -161,8 +161,8 @@
reraise exn
else
{outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
- rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
- z3_proof = []}
+ rewrite_rules = [], conjecture_id = ~1, prem_ids = [], helper_ids = [],
+ fact_ids = [], z3_proof = []}
val death = Timer.checkRealTimer timer
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
@@ -227,8 +227,8 @@
end
val weighted_factss = map (apsnd weight_facts) factss
- val {outcome, filter_result = {conjecture_id, rewrite_rules, helper_ids, fact_ids, z3_proof,
- ...}, used_from, run_time} =
+ val {outcome, filter_result = {rewrite_rules, conjecture_id, prem_ids, helper_ids, fact_ids,
+ z3_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
@@ -245,7 +245,7 @@
val fact_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 thy rewrite_rules conjecture_id
+ val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules prem_ids conjecture_id
fact_ids z3_proof
val isar_params =
K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,