--- a/src/HOL/Tools/transfer.ML Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/transfer.ML Sat Apr 16 16:15:37 2011 +0200
@@ -118,7 +118,7 @@
|> Variable.declare_thm thm
|> Variable.declare_term (term_of a)
|> Variable.declare_term (term_of D);
- val certify = Thm.cterm_of (ProofContext.theory_of ctxt3);
+ val certify = Thm.cterm_of (Proof_Context.theory_of ctxt3);
val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso
not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []);
val c_vars = map (certify o Var) vars;