src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML

--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Mar 06 15:58:56 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 (Proof_Context.cterm_of ctxt (mk v)) else NONE)
+         if pred v then SOME (Thm.cterm_of ctxt (mk v)) else NONE)
 
   fun close vars f ct ctxt =
     let