src/HOL/Nominal/nominal_inductive.ML

     val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
     val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
     val fsT = TFree (fs_ctxt_tyname, ind_sort);
 
     val inductive_forall_def' = Drule.instantiate'
-      [SOME (Thm.ctyp_of thy fsT)] [] inductive_forall_def;
+      [SOME (Thm.global_ctyp_of thy fsT)] [] inductive_forall_def;
 
     fun lift_pred' t (Free (s, T)) ts =
       list_comb (Free (s, fsT --> T), t :: ts);
     val lift_pred = lift_pred' (Bound 0);
 

                      else pi2
                    end;
                  val pis'' = fold (concat_perm #> map) pis' pis;
                  val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp)
                    (Vartab.empty, Vartab.empty);
-                 val ihyp' = Thm.instantiate ([], map (apply2 (Thm.cterm_of thy))
+                 val ihyp' = Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy))
                    (map (Envir.subst_term env) vs ~~
                     map (fold_rev (NominalDatatype.mk_perm [])
                       (rev pis' @ pis)) params' @ [z])) ihyp;
                  fun mk_pi th =
                    Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
                        addsimprocs [NominalDatatype.perm_simproc])
                      (Simplifier.simplify (put_simpset eqvt_ss ctxt')
-                       (fold_rev (mk_perm_bool o Thm.cterm_of thy)
+                       (fold_rev (mk_perm_bool o Thm.global_cterm_of thy)
                          (rev pis' @ pis) th));
                  val (gprems1, gprems2) = split_list
                    (map (fn (th, t) =>
                       if null (preds_of ps t) then (SOME th, mk_pi th)
                       else

                     (obtain_fresh_name (args @ map fst qs @ params'))
                     (map snd qs) ([], [], ctxt2);
                   val freshs2' = NominalDatatype.mk_not_sym freshs2;
                   val pis = map (NominalDatatype.perm_of_pair)
                     ((freshs1 ~~ map fst qs) @ (params' ~~ freshs1));
-                  val mk_pis = fold_rev mk_perm_bool (map (Thm.cterm_of thy) pis);
-                  val obj = Thm.cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
+                  val mk_pis = fold_rev mk_perm_bool (map (Thm.global_cterm_of thy) pis);
+                  val obj = Thm.global_cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
                      (fn x as Free _ =>
                            if member (op =) args x then x
                            else (case AList.lookup op = tab x of
                              SOME y => y
                            | NONE => fold_rev (NominalDatatype.mk_perm []) pis x)

         val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
           let
             val prems' = map (fn th => the_default th (map_thm ctxt''
               (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
             val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
-              (mk_perm_bool (Thm.cterm_of thy pi) th)) prems';
-            val intr' = Drule.cterm_instantiate (map (Thm.cterm_of thy) vs ~~
-               map (Thm.cterm_of thy o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
+              (mk_perm_bool (Thm.global_cterm_of thy pi) th)) prems';
+            val intr' = Drule.cterm_instantiate (map (Thm.global_cterm_of thy) vs ~~
+               map (Thm.global_cterm_of thy o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
                intr
           in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1
           end) ctxt' 1 st
       in
         case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of