src/Pure/Isar/generic_target.ML

 fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
     (*term and type parameters*)
-    val ((defs, _), rhs') = Proof_Context.cterm_of lthy rhs
+    val ((defs, _), rhs') = Thm.cterm_of lthy rhs
       |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
 
     val xs = Variable.add_fixed lthy rhs' [];
     val T = Term.fastype_of rhs;
     val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);

       |> Local_Defs.add_def ((b, NoSyn), lhs');
 
     (*result*)
     val def =
       Thm.transitive local_def global_def
-      |> Local_Defs.contract lthy3 defs (Proof_Context.cterm_of lthy3 (Logic.mk_equals (lhs, rhs)));
+      |> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs)));
     val ([(res_name, [res])], lthy4) = lthy3
       |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
   in ((lhs, (res_name, res)), lthy4) end;
 
 

 
     (*export fixes*)
     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
     val frees = map Free (Thm.fold_terms Term.add_frees th' []);
     val (th'' :: vs) =
-      (th' :: map (Drule.mk_term o Proof_Context.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
+      (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
       |> Variable.export ctxt thy_ctxt
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
     val result = Global_Theory.name_thm true true name th'';

       |>> map Logic.dest_type;
 
     val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
     val inst = filter (is_Var o fst) (vars ~~ frees);
     val cinstT = instT
-      |> map (apply2 (Proof_Context.ctyp_of ctxt) o apfst TVar);
+      |> map (apply2 (Thm.ctyp_of ctxt) o apfst TVar);
     val cinst = inst
-      |> map (apply2 (Proof_Context.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT)));
+      |> map (apply2 (Thm.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT)));
     val result' = Thm.instantiate (cinstT, cinst) result;
 
     (*import assumes/defines*)
     val result'' =
       (fold (curry op COMP) asms' result'