src/HOL/Nominal/nominal_atoms.ML

     val thy1 = TypedefPackage.add_typedecls (map (fn x => (x,[],NoSyn)) ak_names) thy;
     
     (* produces a list consisting of pairs:         *)
     (*  fst component is the atom-kind name         *)
     (*  snd component is its type                   *)
-    val full_ak_names = map (Sign.intern_type (sign_of thy1)) ak_names;
+    val full_ak_names = map (Sign.intern_type thy1) ak_names;
     val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names;
      
     (* adds for every atom-kind an axiom             *)
     (* <ak>_infinite: infinite (UNIV::<ak_type> set) *)
     val (inf_axs,thy2) = PureThy.add_axioms_i (map (fn (ak_name, T) =>

     (* swap_<ak> (a,b) c = (if a=c then b (else if b=c then a else c)) *)
     (* overloades then the general swap-function                       *) 
     val (swap_eqs, thy3) = fold_map (fn (ak_name, T) => fn thy =>
       let
         val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
-        val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name);
+        val swap_name = Sign.full_name thy ("swap_" ^ ak_name);
         val a = Free ("a", T);
         val b = Free ("b", T);
         val c = Free ("c", T);
         val ab = Free ("ab", HOLogic.mk_prodT (T, T))
         val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);

     (* <ak>_prm_<ak> []     a = a                                  *)
     (* <ak>_prm_<ak> (x#xs) a = swap_<ak> x (perm xs a)            *)
     val (prm_eqs, thy4) = fold_map (fn (ak_name, T) => fn thy =>
       let
         val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
-        val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name)
+        val swap_name = Sign.full_name thy ("swap_" ^ ak_name)
         val prmT = mk_permT T --> T --> T;
         val prm_name = ak_name ^ "_prm_" ^ ak_name;
-        val qu_prm_name = Sign.full_name (sign_of thy) prm_name;
+        val qu_prm_name = Sign.full_name thy prm_name;
         val x  = Free ("x", HOLogic.mk_prodT (T, T));
         val xs = Free ("xs", mk_permT T);
         val a  = Free ("a", T) ;
 
         val cnil  = Const ("List.list.Nil", mk_permT T);

         let
           val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
           val pi = Free ("pi", mk_permT T);
           val a  = Free ("a", T');
           val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
-          val cperm_def = Const (Sign.full_name (sign_of thy') perm_def_name, mk_permT T --> T' --> T');
+          val cperm_def = Const (Sign.full_name thy' perm_def_name, mk_permT T --> T' --> T');
 
           val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
           val def = Logic.mk_equals
                     (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
         in

     (* lemma at_<ak>_inst:                              *)
     (* at TYPE(<ak>)                                    *)
     val (prm_cons_thms,thy6) = 
       thy5 |> PureThy.add_thms (map (fn (ak_name, T) =>
       let
-        val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);
+        val ak_name_qu = Sign.full_name thy5 (ak_name);
         val i_type = Type(ak_name_qu,[]);
 	val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
         val at_type = Logic.mk_type i_type;
         val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy5
                                   [Name "at_def",

     (* lemma pt_<ak>_inst:                                    *)
     (* pt TYPE('x::pt_<ak>) TYPE(<ak>)                        *)
     val (prm_inst_thms,thy8) = 
       thy7 |> PureThy.add_thms (map (fn (ak_name, T) =>
       let
-        val ak_name_qu = Sign.full_name (sign_of thy7) (ak_name);
-        val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name);
+        val ak_name_qu = Sign.full_name thy7 ak_name;
+        val pt_name_qu = Sign.full_name thy7 ("pt_"^ak_name);
         val i_type1 = TFree("'x",[pt_name_qu]);
         val i_type2 = Type(ak_name_qu,[]);
 	val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
         val pt_type = Logic.mk_type i_type1;
         val at_type = Logic.mk_type i_type2;

      (* axclass fs_<ak>                                  *)
      (* fs_<ak>1: finite ((supp x)::<ak> set)            *)
      val (fs_ax_classes,thy11) =  fold_map (fn (ak_name, T) => fn thy =>
        let 
 	  val cl_name = "fs_"^ak_name;
-	  val pt_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+	  val pt_name = Sign.full_name thy ("pt_"^ak_name);
           val ty = TFree("'a",["HOL.type"]);
           val x   = Free ("x", ty);
           val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
           val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
           

      (* lemma abst_<ak>_inst:                                    *)
      (* fs TYPE('x::pt_<ak>) TYPE (<ak>)                         *)
      val (fs_inst_thms,thy12) = 
        thy11 |> PureThy.add_thms (map (fn (ak_name, T) =>
        let
-         val ak_name_qu = Sign.full_name (sign_of thy11) (ak_name);
-         val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name);
+         val ak_name_qu = Sign.full_name thy11 ak_name;
+         val fs_name_qu = Sign.full_name thy11 ("fs_"^ak_name);
          val i_type1 = TFree("'x",[fs_name_qu]);
          val i_type2 = Type(ak_name_qu,[]);
  	 val cfs = Const ("Nominal.fs", 
                                  (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
          val fs_type = Logic.mk_type i_type1;

         (* lemma cp_<ak1>_<ak2>_inst:                                           *)
         (* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>)                  *)
         val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy =>
 	 fold_map (fn (ak_name', T') => fn thy' =>
            let
-             val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
-	     val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
-             val cp_name_qu  = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+             val ak_name_qu  = Sign.full_name thy' (ak_name);
+	     val ak_name_qu' = Sign.full_name thy' (ak_name');
+             val cp_name_qu  = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
              val i_type0 = TFree("'a",[cp_name_qu]);
              val i_type1 = Type(ak_name_qu,[]);
              val i_type2 = Type(ak_name_qu',[]);
 	     val ccp = Const ("Nominal.cp",
                              (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->

         val (dj_thms, thy12d) = fold_map (fn (ak_name,T) => fn thy =>
 	  fold_map (fn (ak_name',T') => fn thy' =>
           (if not (ak_name = ak_name') 
            then 
 	       let
-		 val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
-	         val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
+		 val ak_name_qu  = Sign.full_name thy' ak_name;
+	         val ak_name_qu' = Sign.full_name thy' ak_name';
                  val i_type1 = Type(ak_name_qu,[]);
                  val i_type2 = Type(ak_name_qu',[]);
 	         val cdj = Const ("Nominal.disjoint",
                            (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
                  val at_type  = Logic.mk_type i_type1;

      (* every <ak> is an instance of pt_<ak'>; the proof for       *)
      (* ak!=ak' is by definition; the case ak=ak' uses at_pt_inst. *)
      val thy13 = fold (fn ak_name => fn thy =>
 	fold (fn ak_name' => fn thy' =>
          let
-           val qu_name =  Sign.full_name (sign_of thy') ak_name';
-           val cls_name = Sign.full_name (sign_of thy') ("pt_"^ak_name);
+           val qu_name =  Sign.full_name thy' ak_name';
+           val cls_name = Sign.full_name thy' ("pt_"^ak_name);
            val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name'^"_inst")); 
 
            val proof1 = EVERY [ClassPackage.intro_classes_tac [],
                                  rtac ((at_inst RS at_pt_inst) RS pt1) 1,
                                  rtac ((at_inst RS at_pt_inst) RS pt2) 1,

      (*      unit                       *)
      (*      set(pt_<ak>)               *)
      (* are instances of pt_<ak>        *)
      val thy18 = fold (fn ak_name => fn thy =>
        let
-          val cls_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+          val cls_name = Sign.full_name thy ("pt_"^ak_name);
           val at_thm   = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
           val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
 
           fun pt_proof thm = 
               EVERY [ClassPackage.intro_classes_tac [],

        (* shows that <ak> is an instance of fs_<ak>     *)
        (* uses the theorem at_<ak>_inst                 *)
        val thy20 = fold (fn ak_name => fn thy =>
         fold (fn ak_name' => fn thy' =>
         let
-           val qu_name =  Sign.full_name (sign_of thy') ak_name';
-           val qu_class = Sign.full_name (sign_of thy') ("fs_"^ak_name);
+           val qu_name =  Sign.full_name thy' ak_name';
+           val qu_class = Sign.full_name thy' ("fs_"^ak_name);
            val proof =
                (if ak_name = ak_name'
                 then
                   let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
                   in  EVERY [ClassPackage.intro_classes_tac [],

        (*    option(fs_<ak>)          *) 
        (* are instances of fs_<ak>    *)
 
        val thy24 = fold (fn ak_name => fn thy => 
         let
-          val cls_name = Sign.full_name (sign_of thy) ("fs_"^ak_name);
+          val cls_name = Sign.full_name thy ("fs_"^ak_name);
           val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
           fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1];
 
           val fs_thm_unit  = fs_unit_inst;
           val fs_thm_prod  = fs_inst RS (fs_inst RS fs_prod_inst);

        (* for every  <ak>/<ai>-combination                *)
        val thy25 = fold (fn ak_name => fn thy =>
          fold (fn ak_name' => fn thy' =>
           fold (fn ak_name'' => fn thy'' =>
             let
-              val name =  Sign.full_name (sign_of thy'') ak_name;
-              val cls_name = Sign.full_name (sign_of thy'') ("cp_"^ak_name'^"_"^ak_name'');
+              val name =  Sign.full_name thy'' ak_name;
+              val cls_name = Sign.full_name thy'' ("cp_"^ak_name'^"_"^ak_name'');
               val proof =
                 (if (ak_name'=ak_name'') then 
                   (let
                     val pt_inst  = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
                     val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));

        (*      noptions                                                 *)
        (* are instances of cp_<ak>_<ai> for every <ak>/<ai>-combination *)
        val thy26 = fold (fn ak_name => fn thy =>
 	fold (fn ak_name' => fn thy' =>
         let
-            val cls_name = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+            val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
             val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
             val pt_inst  = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
             val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
 
             fun cp_proof thm  = EVERY [ClassPackage.intro_classes_tac [],rtac (thm RS cp1) 1];

      val thy32 =
         let
 	  fun discrete_pt_inst discrete_ty defn =
 	     fold (fn ak_name => fn thy =>
 	     let
-	       val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+	       val qu_class = Sign.full_name thy ("pt_"^ak_name);
 	       val simp_s = HOL_basic_ss addsimps [defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
              in 
 	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
              end) ak_names;
 
           fun discrete_fs_inst discrete_ty defn = 
 	     fold (fn ak_name => fn thy =>
 	     let
-	       val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
+	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
 	       val supp_def = thm "Nominal.supp_def";
                val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
              in 
 	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
              end) ak_names;
 
           fun discrete_cp_inst discrete_ty defn = 
 	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
 	     let
-	       val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
+	       val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
 	       val supp_def = thm "Nominal.supp_def";
                val simp_s = HOL_ss addsimps [defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
              in
 	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy