src/HOL/Nominal/nominal_package.ML

         val (bT as Type (b, []), _) = dest_permT U
       in if aT mem permTs_of u andalso aT <> bT then
           let
             val a' = Sign.base_name a;
             val b' = Sign.base_name b;
-            val cp = dynamic_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst");
-            val dj = dynamic_thm thy ("dj_" ^ b' ^ "_" ^ a');
+            val cp = PureThy.get_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst");
+            val dj = PureThy.get_thm thy ("dj_" ^ b' ^ "_" ^ a');
             val dj_cp' = [cp, dj] MRS dj_cp;
             val cert = SOME o cterm_of thy
           in
             SOME (mk_meta_eq (Drule.instantiate' [SOME (ctyp_of thy S)]
               [cert t, cert r, cert s] dj_cp'))

 
     val _ = warning ("length descr: " ^ string_of_int (length descr));
     val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
 
     val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
-    val perm_fun_def = dynamic_thm thy2 "perm_fun_def";
+    val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def";
 
     val unfolded_perm_eq_thms =
       if length descr = length new_type_names then []
       else map standard (List.drop (split_conj_thm
         (Goal.prove_global thy2 [] []

     (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
 
     val _ = warning "perm_append_thms";
 
     (*FIXME: these should be looked up statically*)
-    val at_pt_inst = dynamic_thm thy2 "at_pt_inst";
-    val pt2 = dynamic_thm thy2 "pt2";
+    val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
+    val pt2 = PureThy.get_thm thy2 "pt2";
 
     val perm_append_thms = List.concat (map (fn a =>
       let
         val permT = mk_permT (Type (a, []));
         val pi1 = Free ("pi1", permT);
         val pi2 = Free ("pi2", permT);
-        val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
+        val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
         val pt2' = pt_inst RS pt2;
-        val pt2_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
+        val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
       in List.take (map standard (split_conj_thm
         (Goal.prove_global thy2 [] []
              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
                 (map (fn ((s, T), x) =>
                     let val perm = Const (s, permT --> T --> T)

 
     (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
 
     val _ = warning "perm_eq_thms";
 
-    val pt3 = dynamic_thm thy2 "pt3";
-    val pt3_rev = dynamic_thm thy2 "pt3_rev";
+    val pt3 = PureThy.get_thm thy2 "pt3";
+    val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
 
     val perm_eq_thms = List.concat (map (fn a =>
       let
         val permT = mk_permT (Type (a, []));
         val pi1 = Free ("pi1", permT);
         val pi2 = Free ("pi2", permT);
         (*FIXME: not robust - better access these theorems using NominalData?*)
-        val at_inst = dynamic_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst");
-        val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
+        val at_inst = PureThy.get_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst");
+        val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
         val pt3' = pt_inst RS pt3;
         val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
-        val pt3_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
+        val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
       in List.take (map standard (split_conj_thm
         (Goal.prove_global thy2 [] [] (Logic.mk_implies
              (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
                 permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
               HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

          length new_type_names)
       end) atoms);
 
     (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
 
-    val cp1 = dynamic_thm thy2 "cp1";
-    val dj_cp = dynamic_thm thy2 "dj_cp";
-    val pt_perm_compose = dynamic_thm thy2 "pt_perm_compose";
-    val pt_perm_compose_rev = dynamic_thm thy2 "pt_perm_compose_rev";
-    val dj_perm_perm_forget = dynamic_thm thy2 "dj_perm_perm_forget";
+    val cp1 = PureThy.get_thm thy2 "cp1";
+    val dj_cp = PureThy.get_thm thy2 "dj_cp";
+    val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose";
+    val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev";
+    val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget";
 
     fun composition_instance name1 name2 thy =
       let
         val name1' = Sign.base_name name1;
         val name2' = Sign.base_name name2;

         val permT1 = mk_permT (Type (name1, []));
         val permT2 = mk_permT (Type (name2, []));
         val augment = map_type_tfree
           (fn (x, S) => TFree (x, cp_class :: S));
         val Ts = map (augment o body_type) perm_types;
-        val cp_inst = dynamic_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst");
+        val cp_inst = PureThy.get_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst");
         val simps = simpset_of thy addsimps (perm_fun_def ::
           (if name1 <> name2 then
-             let val dj = dynamic_thm thy ("dj_" ^ name2' ^ "_" ^ name1')
+             let val dj = PureThy.get_thm thy ("dj_" ^ name2' ^ "_" ^ name1')
              in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
            else
              let
-               val at_inst = dynamic_thm thy ("at_" ^ name1' ^ "_inst");
-               val pt_inst = dynamic_thm thy ("pt_" ^ name1' ^ "_inst");
+               val at_inst = PureThy.get_thm thy ("at_" ^ name1' ^ "_inst");
+               val pt_inst = PureThy.get_thm thy ("pt_" ^ name1' ^ "_inst");
              in
                [cp_inst RS cp1 RS sym,
                 at_inst RS (pt_inst RS pt_perm_compose) RS sym,
                 at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
             end))

 
     (**** Prove that representing set is closed under permutation ****)
 
     val _ = warning "proving closure under permutation...";
 
-    val abs_perm = dynamic_thms thy4 "abs_perm";
+    val abs_perm = PureThy.get_thms thy4 "abs_perm";
 
     val perm_indnames' = List.mapPartial
       (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
       (perm_indnames ~~ descr);
 

             (EVERY [Class.intro_classes_tac [],
               rewrite_goals_tac [perm_def],
               asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
               asm_full_simp_tac (simpset_of thy addsimps
                 [Rep RS perm_closed RS Abs_inverse]) 1,
-              asm_full_simp_tac (HOL_basic_ss addsimps [dynamic_thm thy
+              asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
                 ("pt_" ^ Sign.base_name atom ^ "3")]) 1]) thy)
         (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
            new_type_names ~~ tyvars ~~ perm_closed_thms);
 
 

 
     fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
       let
         val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
         val class = Sign.intern_class thy name;
-        val cp1' = dynamic_thm thy (name ^ "_inst") RS cp1
+        val cp1' = PureThy.get_thm thy (name ^ "_inst") RS cp1
       in fold (fn ((((((Abs_inverse, Rep),
         perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
           AxClass.prove_arity
             (Sign.intern_type thy name,
               replicate (length tvs) (classes @ cp_classes), [class])

       end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
 
     (** prove injectivity of constructors **)
 
     val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
-    val alpha = dynamic_thms thy8 "alpha";
-    val abs_fresh = dynamic_thms thy8 "abs_fresh";
+    val alpha = PureThy.get_thms thy8 "alpha";
+    val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
 
     val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
       let val T = nth_dtyp' i
       in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
         if null dts then NONE else SOME

 
     val _ = warning "proving finite support for the new datatype";
 
     val indnames = DatatypeProp.make_tnames recTs;
 
-    val abs_supp = dynamic_thms thy8 "abs_supp";
-    val supp_atm = dynamic_thms thy8 "supp_atm";
+    val abs_supp = PureThy.get_thms thy8 "abs_supp";
+    val supp_atm = PureThy.get_thms thy8 "supp_atm";
 
     val finite_supp_thms = map (fn atom =>
       let val atomT = Type (atom, [])
       in map standard (List.take
         (split_conj_thm (Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop

                (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
                (indnames ~~ recTs))))
            (fn _ => indtac dt_induct indnames 1 THEN
             ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
               (abs_supp @ supp_atm @
-               dynamic_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
+               PureThy.get_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
                List.concat supp_thms))))),
          length new_type_names))
       end) atoms;
 
     val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];

           fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
             (Free (tname, T))))
         (descr'' ~~ recTs ~~ tnames)));
 
     val fin_set_supp = map (fn Type (s, _) =>
-      dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
+      PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
         at_fin_set_supp) dt_atomTs;
     val fin_set_fresh = map (fn Type (s, _) =>
-      dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
+      PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
         at_fin_set_fresh) dt_atomTs;
     val pt1_atoms = map (fn Type (s, _) =>
-      dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
+      PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
     val pt2_atoms = map (fn Type (s, _) =>
-      dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
-    val exists_fresh' = dynamic_thms thy9 "exists_fresh'";
-    val fs_atoms = dynamic_thms thy9 "fin_supp";
-    val abs_supp = dynamic_thms thy9 "abs_supp";
-    val perm_fresh_fresh = dynamic_thms thy9 "perm_fresh_fresh";
-    val calc_atm = dynamic_thms thy9 "calc_atm";
-    val fresh_atm = dynamic_thms thy9 "fresh_atm";
-    val fresh_left = dynamic_thms thy9 "fresh_left";
-    val perm_swap = dynamic_thms thy9 "perm_swap";
+      PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
+    val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
+    val fs_atoms = PureThy.get_thms thy9 "fin_supp";
+    val abs_supp = PureThy.get_thms thy9 "abs_supp";
+    val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh";
+    val calc_atm = PureThy.get_thms thy9 "calc_atm";
+    val fresh_atm = PureThy.get_thms thy9 "fresh_atm";
+    val fresh_left = PureThy.get_thms thy9 "fresh_left";
+    val perm_swap = PureThy.get_thms thy9 "perm_swap";
 
     fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
       let
         val p = foldr1 HOLogic.mk_prod (ts @ freshs1);
         val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop

       PureThy.hide_thms true [NameSpace.append
         (Sign.full_name thy10 big_rec_name) "induct"];
 
     (** equivariance **)
 
-    val fresh_bij = dynamic_thms thy11 "fresh_bij";
-    val perm_bij = dynamic_thms thy11 "perm_bij";
+    val fresh_bij = PureThy.get_thms thy11 "fresh_bij";
+    val perm_bij = PureThy.get_thms thy11 "perm_bij";
 
     val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
       let
         val permT = mk_permT aT;
         val pi = Free ("pi", permT);

     (** finite support **)
 
     val rec_fin_supp_thms = map (fn aT =>
       let
         val name = Sign.base_name (fst (dest_Type aT));
-        val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1");
+        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
         val aset = HOLogic.mk_setT aT;
         val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
         val fins = map (fn (f, T) => HOLogic.mk_Trueprop
           (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
             (rec_fns ~~ rec_fn_Ts)

            (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
 
     val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
       let
         val name = Sign.base_name (fst (dest_Type aT));
-        val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1");
+        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
         val a = Free ("a", aT);
         val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
           (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)
       in
         map (fn (((T, U), R), eqvt_th) =>