src/Tools/induct.ML

     NONE => NONE
   | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
 
 val rearrange_eqs_simproc =
   Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
-    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of (Proof_Context.theory_of ctxt) t));
+    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.global_cterm_of (Proof_Context.theory_of ctxt) t));
 
 
 (* rotate k premises to the left by j, skipping over first j premises *)
 
 fun rotate_conv 0 j 0 = Conv.all_conv

 
 (* prep_inst *)
 
 fun prep_inst ctxt align tune (tm, ts) =
   let
-    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
+    val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
     fun prep_var (x, SOME t) =
           let
             val cx = cert x;
             val xT = Thm.typ_of_cterm cx;
             val ct = cert (tune t);

 
 local
 
 fun dest_env thy env =
   let
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
+    val cert = Thm.global_cterm_of thy;
+    val certT = Thm.global_ctyp_of thy;
     val pairs = Vartab.dest (Envir.term_env env);
     val types = Vartab.dest (Envir.type_env env);
     val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
     val xs = map2 (curry (cert o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts);
   in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;

   | goal_params _ _ = 0;
 
 fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
   let
     val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
+    val cert = Thm.global_cterm_of thy;
 
     val v = Free (x, T);
     fun spec_rule prfx (xs, body) =
       @{thm Pure.meta_spec}
       |> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1)