diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -103,24 +103,20 @@
    context-independent modulo the current proof context to be able to
    use fast inference kernel rules during proof reconstruction. *)
 
-fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
 val maxidx_of = #maxidx o Thm.rep_cterm
 
 fun mk_inst ctxt vars =
   let
     val max = fold (Integer.max o fst) vars 0
     val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
-    fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
+    fun mk (i, v) = (v, U.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
   in map mk vars end
 
-val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
-
 fun close ctxt (ct, vars) =
   let
     val inst = mk_inst ctxt vars
     val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
-  in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
+  in (U.mk_cprop (Thm.instantiate_cterm ([], inst) ct), names) end
 
 
 fun mk_bound thy (i, T) =
@@ -195,7 +191,7 @@
       |> Symtab.fold (Variable.declare_term o snd) terms
 
     fun cert @{const True} = not_false
-      | cert t = certify ctxt' t
+      | cert t = U.certify ctxt' t
 
   in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
 
@@ -210,7 +206,7 @@
     SOME _ => cx
   | NONE => cx |> fresh_name (decl_prefix ^ n)
       |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
-           let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
+           let val upd = Symtab.update (n, U.certify ctxt (Free (m, T)))
            in (typs, upd terms, exprs, steps, vars, ctxt) end))
 
 fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) =