src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML

--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Wed Mar 04 22:56:25 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Wed Mar 04 23:14:38 2015 +0100
@@ -617,7 +617,7 @@
   fun get_vars f mk pred ctxt t =
     Term.fold_aterms f t []
     |> map_filter (fn v =>
-         if pred v then SOME (Old_SMT_Utils.certify ctxt (mk v)) else NONE)
+         if pred v then SOME (Proof_Context.cterm_of ctxt (mk v)) else NONE)
 
   fun close vars f ct ctxt =
     let