src/Pure/Tools/rule_insts.ML

     (* result *)
 
     val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
     val inst_vars = map_filter (make_inst inst2) vars2;
   in
-    (map (apply2 (Thm.ctyp_of thy)) inst_tvars,
-     map (apply2 (Thm.cterm_of thy)) inst_vars)
+    (map (apply2 (Thm.global_ctyp_of thy)) inst_tvars,
+     map (apply2 (Thm.global_cterm_of thy)) inst_vars)
   end;
 
 fun where_rule ctxt mixed_insts fixes thm =
   let
     val ctxt' = ctxt

         val envT' = map (fn (ixn, T) =>
           (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
         val cenv =
           map
             (fn (xi, t) =>
-              apply2 (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
+              apply2 (Thm.global_cterm_of thy) (Var (xi, fastype_of t), t))
             (distinct
               (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
               (xis ~~ ts));
         (* Lift and instantiate rule *)
         val maxidx = Thm.maxidx_of st;

               Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
           | liftvar t = raise TERM("Variable expected", [t]);
         fun liftterm t =
           fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
         fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
-        val lifttvar = apply2 (Thm.ctyp_of thy o Logic.incr_tvar inc);
+        val lifttvar = apply2 (Thm.global_ctyp_of thy o Logic.incr_tvar inc);
         val rule = Drule.instantiate_normalize
               (map lifttvar envT', map liftpair cenv)
               (Thm.lift_rule cgoal thm)
       in
         compose_tac ctxt' (bires_flag, rule, Thm.nprems_of thm) i

 
 fun make_elim_preserve ctxt rl =
   let
     val thy = Thm.theory_of_thm rl;
     val maxidx = Thm.maxidx_of rl;
-    fun cvar xi = Thm.cterm_of thy (Var (xi, propT));
+    fun cvar xi = Thm.global_cterm_of thy (Var (xi, propT));
     val revcut_rl' =
       Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
         (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   in
     (case Seq.list_of