src/HOL/Nominal/nominal_inductive.ML

         (mk_distinct bvars @
          maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
            (NominalDatatype.fresh_const U T $ u $ t)) bvars)
              (ts ~~ binder_types (fastype_of p)))) prems;
 
-    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
-    val pt2_atoms = map (fn aT => PureThy.get_thm thy
+    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
+    val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
       ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
     val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
       addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
       addsimprocs [mk_perm_bool_simproc ["Fun.id"],
         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
-    val fresh_bij = PureThy.get_thms thy "fresh_bij";
-    val perm_bij = PureThy.get_thms thy "perm_bij";
-    val fs_atoms = map (fn aT => PureThy.get_thm thy
+    val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
+    val perm_bij = Global_Theory.get_thms thy "perm_bij";
+    val fs_atoms = map (fn aT => Global_Theory.get_thm thy
       ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
-    val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
-    val fresh_atm = PureThy.get_thms thy "fresh_atm";
-    val swap_simps = PureThy.get_thms thy "swap_simps";
-    val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh";
+    val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'";
+    val fresh_atm = Global_Theory.get_thms thy "fresh_atm";
+    val swap_simps = Global_Theory.get_thms thy "swap_simps";
+    val perm_fresh_fresh = Global_Theory.get_thms thy "perm_fresh_fresh";
 
     fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) =
       let
         (** protect terms to avoid that fresh_prod interferes with  **)
         (** pairs used in introduction rules of inductive predicate **)

          case subtract (op =) atoms' atoms of
              [] => ()
            | xs => error ("No such atoms: " ^ commas xs);
          atoms)
       end;
-    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
+    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
     val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
       (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
       [mk_perm_bool_simproc names,
        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val (([t], [pi]), ctxt') = ctxt |>