src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
changeset 56981 3ef45ce002b5
parent 56303 4cc3f4db3447
child 56983 132142089ea6
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 17:11:56 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
     1.3 @@ -161,8 +161,8 @@
     1.4                reraise exn
     1.5              else
     1.6                {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
     1.7 -               rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
     1.8 -               z3_proof = []}
     1.9 +               rewrite_rules = [], conjecture_id = ~1, prem_ids = [], helper_ids = [],
    1.10 +               fact_ids = [], z3_proof = []}
    1.11  
    1.12          val death = Timer.checkRealTimer timer
    1.13          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
    1.14 @@ -227,8 +227,8 @@
    1.15        end
    1.16  
    1.17      val weighted_factss = map (apsnd weight_facts) factss
    1.18 -    val {outcome, filter_result = {conjecture_id, rewrite_rules, helper_ids, fact_ids, z3_proof,
    1.19 -           ...}, used_from, run_time} =
    1.20 +    val {outcome, filter_result = {rewrite_rules, conjecture_id, prem_ids, helper_ids, fact_ids,
    1.21 +           z3_proof, ...}, used_from, run_time} =
    1.22        smt2_filter_loop name params state goal subgoal weighted_factss
    1.23      val used_named_facts = map snd fact_ids
    1.24      val used_facts = map fst used_named_facts
    1.25 @@ -245,7 +245,7 @@
    1.26                val fact_ids =
    1.27                  map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
    1.28                  map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    1.29 -              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules conjecture_id
    1.30 +              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules prem_ids conjecture_id
    1.31                  fact_ids z3_proof
    1.32                val isar_params =
    1.33                  K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,