src/HOL/Tools/legacy_transfer.ML

   (inj, embed, return, cong);
 
 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';
       in a aconvc a' andalso D aconvc D' end;
   in case AList.lookup eq_direction (Data.get context) (a0, D0) of

       |> Variable.declare_thm thm
       |> Variable.declare_term (Thm.term_of a)
       |> 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 *)
     val (hyps, ctxt5) = ctxt4
       |> Assumption.add_assumes (map transform c_vars');