1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Oct 26 11:31:03 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Oct 26 11:39:26 2010 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    val add_z3_rule: thm -> Context.generic -> Context.generic
     1.5    val trace_assms: bool Config.T
     1.6    val reconstruct: string list * SMT_Translate.recon -> Proof.context ->
     1.7 -    thm * Proof.context
     1.8 +    (int list * thm) * Proof.context
     1.9    val setup: theory -> theory
    1.10  end
    1.11  
    1.12 @@ -750,7 +750,7 @@
    1.13  
    1.14  fun prove ctxt unfolds assms vars =
    1.15    let
    1.16 -    val assms' = prepare_assms ctxt unfolds assms
    1.17 +    val assms' = prepare_assms ctxt unfolds (map snd assms) (* FIXME *)
    1.18      val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt)
    1.19  
    1.20      fun step r ps ct (cxp as (cx, ptab)) =
    1.21 @@ -821,7 +821,7 @@
    1.22        | SOME (Proved p) => (p, cxp)
    1.23        | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
    1.24  
    1.25 -    fun result (p, (cx, _)) = (thm_of p, cx)
    1.26 +    fun result (p, (cx, _)) = (([], thm_of p), cx) (*FIXME*)
    1.27    in
    1.28      (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab)))
    1.29    end