src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
changeset 56983 132142089ea6
parent 56981 3ef45ce002b5
child 56984 d20f19f54789
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
     1.3 @@ -221,6 +221,8 @@
     1.4      val thy = Proof.theory_of state
     1.5      val ctxt = Proof.context_of state
     1.6  
     1.7 +    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
     1.8 +
     1.9      fun weight_facts facts =
    1.10        let val num_facts = length facts in
    1.11          map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
    1.12 @@ -245,8 +247,8 @@
    1.13                val fact_ids =
    1.14                  map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
    1.15                  map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    1.16 -              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules prem_ids conjecture_id
    1.17 -                fact_ids z3_proof
    1.18 +              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t
    1.19 +                prem_ids conjecture_id fact_ids z3_proof
    1.20                val isar_params =
    1.21                  K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
    1.22                     minimize <> SOME false, atp_proof, goal)