--- a/src/HOL/Tools/legacy_transfer.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/legacy_transfer.ML Fri Mar 06 15:58:56 2015 +0100
@@ -59,8 +59,8 @@
fun get_by_direction context (a, D) =
let
val ctxt = Context.proof_of context;
- val a0 = Proof_Context.cterm_of ctxt a;
- val D0 = Proof_Context.cterm_of ctxt D;
+ val a0 = Thm.cterm_of ctxt a;
+ val D0 = Thm.cterm_of ctxt D;
fun eq_direction ((a, D), thm') =
let
val (a', D') = direction_of thm';
@@ -118,9 +118,9 @@
|> Variable.declare_term (Thm.term_of D);
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 (Proof_Context.cterm_of ctxt3 o Var) vars;
+ val c_vars = map (Thm.cterm_of ctxt3 o Var) vars;
val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
- val c_vars' = map (Proof_Context.cterm_of ctxt3 o (fn v => Free (v, bT))) vs';
+ val c_vars' = map (Thm.cterm_of ctxt3 o (fn v => Free (v, bT))) vs';
val c_exprs' = map (Thm.apply a) c_vars';
(* transfer *)