src/HOL/Nominal/nominal_atoms.ML

 
 fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
 
 fun mk_Cons x xs =
   let val T = fastype_of x
-  in Const (@{const_name Cons}, T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
+  in Const (\<^const_name>\<open>Cons\<close>, T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
 
 fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args);
 fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args);
 
 (* this function sets up all matters related to atom-  *)

 fun create_nom_typedecls ak_names thy =
   let
     
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
-          let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
+          let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [\<^typ>\<open>nat\<close>], NoSyn)])
               val (dt_names, thy1) = BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Kill_Type_Args] [dt] thy;
             
               val injects = maps (#inject o BNF_LFP_Compat.the_info thy1 []) dt_names;
               val ak_type = Type (Sign.intern_type thy1 ak,[])
               val ak_sign = Sign.intern_const thy1 ak 
               
-              val inj_type = @{typ nat} --> ak_type
-              val inj_on_type = inj_type --> @{typ "nat set"} --> @{typ bool}
+              val inj_type = \<^typ>\<open>nat\<close> --> ak_type
+              val inj_on_type = inj_type --> \<^typ>\<open>nat set\<close> --> \<^typ>\<open>bool\<close>
 
               (* first statement *)
               val stmnt1 = HOLogic.mk_Trueprop 
-                  (Const (@{const_name "inj_on"},inj_on_type) $ 
-                         Const (ak_sign,inj_type) $ HOLogic.mk_UNIV @{typ nat})
+                  (Const (\<^const_name>\<open>inj_on\<close>,inj_on_type) $ 
+                         Const (ak_sign,inj_type) $ HOLogic.mk_UNIV \<^typ>\<open>nat\<close>)
 
               val simp1 = @{thm inj_on_def} :: injects;
               
               fun proof1 ctxt = EVERY [simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1,
                 resolve_tac ctxt @{thms ballI} 1,

                    add_thms_string [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 (proof1 o #context)), [])] thy1
               
               (* second statement *)
               val y = Free ("y",ak_type)  
               val stmnt2 = HOLogic.mk_Trueprop
-                  (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
+                  (HOLogic.mk_exists ("x",\<^typ>\<open>nat\<close>,HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
 
               val proof2 = fn {prems, context = ctxt} =>
                 Induct_Tacs.case_tac ctxt "y" [] NONE 1 THEN
                 asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN
                 resolve_tac ctxt @{thms exI} 1 THEN

               val (inject_thm,thy3) =
                   add_thms_string [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2
   
               val stmnt3 = HOLogic.mk_Trueprop
                            (HOLogic.mk_not
-                              (Const (@{const_name finite}, HOLogic.mk_setT ak_type --> HOLogic.boolT) $
+                              (Const (\<^const_name>\<open>finite\<close>, HOLogic.mk_setT ak_type --> HOLogic.boolT) $
                                   HOLogic.mk_UNIV ak_type))
              
               val simp2 = [@{thm image_def},@{thm bex_UNIV}]@inject_thm
               val simp3 = [@{thm UNIV_def}]
 

         val full_swap_name = Sign.full_bname thy' swap_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 (@{const_name If}, HOLogic.boolT --> T --> T --> T);
+        val cif = Const (\<^const_name>\<open>If\<close>, HOLogic.boolT --> T --> T --> T);
         val cswap_akname = Const (full_swap_name, swapT);
-        val cswap = Const (@{const_name Nominal.swap}, swapT)
+        val cswap = Const (\<^const_name>\<open>Nominal.swap\<close>, swapT)
 
         val name = swap_name ^ "_def";
         val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
                 (Free (swap_name, swapT) $ HOLogic.mk_prod (a,b) $ c,
                     cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))

         val prm = Free (prm_name, prmT);
         val x  = Free ("x", HOLogic.mk_prodT (T, T));
         val xs = Free ("xs", mk_permT T);
         val a  = Free ("a", T) ;
 
-        val cnil  = Const (@{const_name Nil}, mk_permT T);
+        val cnil  = Const (\<^const_name>\<open>Nil\<close>, mk_permT T);
         
         val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (prm $ cnil $ a, a));
 
         val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
                    (prm $ mk_Cons x xs $ a,

       fold_map (fn (ak_name', T') => fn thy' =>
         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 (@{const_name Nominal.perm}, mk_permT T --> T' --> T');
+          val cperm = Const (\<^const_name>\<open>Nominal.perm\<close>, mk_permT T --> T' --> T');
           val thy'' = Sign.add_path "rec" thy'
           val cperm_def = Const (Sign.full_bname thy'' perm_def_name, mk_permT T --> T' --> T');
           val thy''' = Sign.parent_path thy'';
 
           val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";

     val (prm_cons_thms,thy6) = 
       thy5 |> add_thms_string (map (fn (ak_name, T) =>
       let
         val ak_name_qu = Sign.full_bname thy5 (ak_name);
         val i_type = Type(ak_name_qu,[]);
-        val cat = Const (@{const_name Nominal.at}, Term.itselfT i_type --> HOLogic.boolT);
+        val cat = Const (\<^const_name>\<open>Nominal.at\<close>, Term.itselfT i_type --> HOLogic.boolT);
         val at_type = Logic.mk_type i_type;
         fun proof ctxt =
           simp_tac (put_simpset HOL_ss ctxt
             addsimps maps (Global_Theory.get_thms thy5)
                                   ["at_def",

     (* pt_<ak>2:       perm (pi1@pi2) x = perm pi1 (perm pi2 x)  *)
     (* pt_<ak>3:       pi1 ~ pi2 ==> perm pi1 x = perm pi2 x     *)
      val (pt_ax_classes,thy7) =  fold_map (fn (ak_name, T) => fn thy =>
       let 
           val cl_name = "pt_"^ak_name;
-          val ty = TFree("'a", @{sort type});
+          val ty = TFree("'a", \<^sort>\<open>type\<close>);
           val x   = Free ("x", ty);
           val pi1 = Free ("pi1", mk_permT T);
           val pi2 = Free ("pi2", mk_permT T);
-          val cperm = Const (@{const_name Nominal.perm}, mk_permT T --> ty --> ty);
-          val cnil  = Const (@{const_name Nil}, mk_permT T);
-          val cappend = Const (@{const_name append}, mk_permT T --> mk_permT T --> mk_permT T);
-          val cprm_eq = Const (@{const_name Nominal.prm_eq}, mk_permT T --> mk_permT T --> HOLogic.boolT);
+          val cperm = Const (\<^const_name>\<open>Nominal.perm\<close>, mk_permT T --> ty --> ty);
+          val cnil  = Const (\<^const_name>\<open>Nil\<close>, mk_permT T);
+          val cappend = Const (\<^const_name>\<open>append\<close>, mk_permT T --> mk_permT T --> mk_permT T);
+          val cprm_eq = Const (\<^const_name>\<open>Nominal.prm_eq\<close>, mk_permT T --> mk_permT T --> HOLogic.boolT);
           (* nil axiom *)
           val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
                        (cperm $ cnil $ x, x));
           (* append axiom *)
           val axiom2 = HOLogic.mk_Trueprop (HOLogic.mk_eq

           (* perm-eq axiom *)
           val axiom3 = Logic.mk_implies
                        (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
                         HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
       in
-          Axclass.define_class (Binding.name cl_name, @{sort type}) []
+          Axclass.define_class (Binding.name cl_name, \<^sort>\<open>type\<close>) []
                 [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
                  ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
                  ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
       end) ak_names_types thy6;
 

         val ak_name_qu = Sign.full_bname thy7 ak_name;
         val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name);
         val i_type1 = TFree("'x",[pt_name_qu]);
         val i_type2 = Type(ak_name_qu,[]);
         val cpt =
-          Const (@{const_name Nominal.pt}, (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
+          Const (\<^const_name>\<open>Nominal.pt\<close>, (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;
         fun proof ctxt =
           simp_tac (put_simpset HOL_ss ctxt addsimps maps (Global_Theory.get_thms thy7)
                                   ["pt_def",

      (* 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_bname thy ("pt_"^ak_name);
-          val ty = TFree("'a",@{sort type});
+          val ty = TFree("'a",\<^sort>\<open>type\<close>);
           val x   = Free ("x", ty);
-          val csupp    = Const (@{const_name Nominal.supp}, ty --> HOLogic.mk_setT T);
-          val cfinite  = Const (@{const_name finite}, HOLogic.mk_setT T --> HOLogic.boolT)
+          val csupp    = Const (\<^const_name>\<open>Nominal.supp\<close>, ty --> HOLogic.mk_setT T);
+          val cfinite  = Const (\<^const_name>\<open>finite\<close>, HOLogic.mk_setT T --> HOLogic.boolT)
           
           val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
 
        in  
         Axclass.define_class (Binding.name cl_name, [pt_name]) []

        let
          val ak_name_qu = Sign.full_bname thy11 ak_name;
          val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name);
          val i_type1 = TFree("'x",[fs_name_qu]);
          val i_type2 = Type(ak_name_qu,[]);
-         val cfs = Const (@{const_name Nominal.fs},
+         val cfs = Const (\<^const_name>\<open>Nominal.fs\<close>,
                                  (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
          val fs_type = Logic.mk_type i_type1;
          val at_type = Logic.mk_type i_type2;
          fun proof ctxt =
           simp_tac (put_simpset HOL_ss ctxt addsimps maps (Global_Theory.get_thms thy11)

        (* cp_<ak1>_<ak2>1: pi1 o pi2 o x = (pi1 o pi2) o (pi1 o x)       *)
         val (cp_ax_classes,thy12b) = fold_map (fn (ak_name, T) => fn thy =>
          fold_map (fn (ak_name', T') => fn thy' =>
              let
                val cl_name = "cp_"^ak_name^"_"^ak_name';
-               val ty = TFree("'a",@{sort type});
+               val ty = TFree("'a",\<^sort>\<open>type\<close>);
                val x   = Free ("x", ty);
                val pi1 = Free ("pi1", mk_permT T);
                val pi2 = Free ("pi2", mk_permT T');                  
-               val cperm1 = Const (@{const_name Nominal.perm}, mk_permT T  --> ty --> ty);
-               val cperm2 = Const (@{const_name Nominal.perm}, mk_permT T' --> ty --> ty);
-               val cperm3 = Const (@{const_name Nominal.perm}, mk_permT T  --> mk_permT T' --> mk_permT T');
+               val cperm1 = Const (\<^const_name>\<open>Nominal.perm\<close>, mk_permT T  --> ty --> ty);
+               val cperm2 = Const (\<^const_name>\<open>Nominal.perm\<close>, mk_permT T' --> ty --> ty);
+               val cperm3 = Const (\<^const_name>\<open>Nominal.perm\<close>, mk_permT T  --> mk_permT T' --> mk_permT T');
 
                val ax1   = HOLogic.mk_Trueprop 
                            (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
                                            cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
                in  
-                 Axclass.define_class (Binding.name cl_name, @{sort type}) []
+                 Axclass.define_class (Binding.name cl_name, \<^sort>\<open>type\<close>) []
                    [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'  
                end) ak_names_types thy) ak_names_types thy12;
 
         (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)
         (* lemma cp_<ak1>_<ak2>_inst:                                           *)

              val ak_name_qu' = Sign.full_bname thy' (ak_name');
              val cp_name_qu  = Sign.full_bname 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 (@{const_name Nominal.cp},
+             val ccp = Const (\<^const_name>\<open>Nominal.cp\<close>,
                              (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
                                                       (Term.itselfT i_type2)-->HOLogic.boolT);
              val at_type  = Logic.mk_type i_type1;
              val at_type' = Logic.mk_type i_type2;
              val cp_type  = Logic.mk_type i_type0;

                let
                  val ak_name_qu  = Sign.full_bname thy' ak_name;
                  val ak_name_qu' = Sign.full_bname thy' ak_name';
                  val i_type1 = Type(ak_name_qu,[]);
                  val i_type2 = Type(ak_name_qu',[]);
-                 val cdj = Const (@{const_name Nominal.disjoint},
+                 val cdj = Const (\<^const_name>\<open>Nominal.disjoint\<close>,
                            (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
                  val at_type  = Logic.mk_type i_type1;
                  val at_type' = Logic.mk_type i_type2;
                  fun proof ctxt =
                   simp_tac (put_simpset HOL_ss ctxt

           val pt_thm_prod  = pt_inst RS (pt_inst RS pt_prod_inst);
           val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst);
           val pt_thm_unit  = pt_unit_inst;
        in
         thy
-        |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
-        |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
-        |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
-        |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
-        |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
-        |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
-        |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_nprod)
-        |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (pt_proof pt_thm_unit)
+        |> Axclass.prove_arity (\<^type_name>\<open>fun\<close>,[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
+        |> Axclass.prove_arity (\<^type_name>\<open>set\<close>,[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
+        |> Axclass.prove_arity (\<^type_name>\<open>noption\<close>,[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
+        |> Axclass.prove_arity (\<^type_name>\<open>option\<close>,[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
+        |> Axclass.prove_arity (\<^type_name>\<open>list\<close>,[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
+        |> Axclass.prove_arity (\<^type_name>\<open>prod\<close>,[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+        |> Axclass.prove_arity (\<^type_name>\<open>nprod\<close>,[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_nprod)
+        |> Axclass.prove_arity (\<^type_name>\<open>unit\<close>,[],[cls_name]) (pt_proof pt_thm_unit)
      end) ak_names thy13; 
 
        (********  fs_<ak> class instances  ********)
        (*=========================================*)
        (* abbreviations for some lemmas *)

           val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst);
           val fs_thm_list  = fs_inst RS fs_list_inst;
           val fs_thm_optn  = fs_inst RS fs_option_inst;
         in 
          thy
-         |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (fs_proof fs_thm_unit) 
-         |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
-         |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_nprod)
-         |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
-         |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
+         |> Axclass.prove_arity (\<^type_name>\<open>unit\<close>,[],[cls_name]) (fs_proof fs_thm_unit) 
+         |> Axclass.prove_arity (\<^type_name>\<open>prod\<close>,[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
+         |> Axclass.prove_arity (\<^type_name>\<open>nprod\<close>,[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_nprod)
+         |> Axclass.prove_arity (\<^type_name>\<open>list\<close>,[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
+         |> Axclass.prove_arity (\<^type_name>\<open>option\<close>,[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
         end) ak_names thy20;
 
        (********  cp_<ak>_<ai> class instances  ********)
        (*==============================================*)
        (* abbreviations for some lemmas *)

             val cp_thm_optn = cp_inst RS cp_option_inst;
             val cp_thm_noptn = cp_inst RS cp_noption_inst;
             val cp_thm_set = cp_inst RS cp_set_inst;
         in
          thy'
-         |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (cp_proof cp_thm_unit)
-         |> Axclass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
-         |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
-         |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
-         |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
-         |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
-         |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
+         |> Axclass.prove_arity (\<^type_name>\<open>unit\<close>,[],[cls_name]) (cp_proof cp_thm_unit)
+         |> Axclass.prove_arity (\<^type_name>\<open>Product_Type.prod\<close>, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
+         |> Axclass.prove_arity (\<^type_name>\<open>list\<close>,[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
+         |> Axclass.prove_arity (\<^type_name>\<open>fun\<close>,[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
+         |> Axclass.prove_arity (\<^type_name>\<open>option\<close>,[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
+         |> Axclass.prove_arity (\<^type_name>\<open>noption\<close>,[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+         |> Axclass.prove_arity (\<^type_name>\<open>set\<close>,[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
         end) ak_names thy) ak_names thy25;
 
      (* show that discrete nominal types are permutation types, finitely     *)
      (* supported and have the commutation property                          *)
      (* discrete types have a permutation operation defined as pi o x = x;   *)

                Axclass.prove_arity (discrete_ty, [], [qu_class]) proof thy
              end) ak_names)) ak_names;
 
         in
          thy26
-         |> discrete_pt_inst @{type_name nat} @{thm perm_nat_def}
-         |> discrete_fs_inst @{type_name nat} @{thm perm_nat_def}
-         |> discrete_cp_inst @{type_name nat} @{thm perm_nat_def}
-         |> discrete_pt_inst @{type_name bool} @{thm perm_bool_def}
-         |> discrete_fs_inst @{type_name bool} @{thm perm_bool_def}
-         |> discrete_cp_inst @{type_name bool} @{thm perm_bool_def}
-         |> discrete_pt_inst @{type_name int} @{thm perm_int_def}
-         |> discrete_fs_inst @{type_name int} @{thm perm_int_def}
-         |> discrete_cp_inst @{type_name int} @{thm perm_int_def}
-         |> discrete_pt_inst @{type_name char} @{thm perm_char_def}
-         |> discrete_fs_inst @{type_name char} @{thm perm_char_def}
-         |> discrete_cp_inst @{type_name char} @{thm perm_char_def}
+         |> discrete_pt_inst \<^type_name>\<open>nat\<close> @{thm perm_nat_def}
+         |> discrete_fs_inst \<^type_name>\<open>nat\<close> @{thm perm_nat_def}
+         |> discrete_cp_inst \<^type_name>\<open>nat\<close> @{thm perm_nat_def}
+         |> discrete_pt_inst \<^type_name>\<open>bool\<close> @{thm perm_bool_def}
+         |> discrete_fs_inst \<^type_name>\<open>bool\<close> @{thm perm_bool_def}
+         |> discrete_cp_inst \<^type_name>\<open>bool\<close> @{thm perm_bool_def}
+         |> discrete_pt_inst \<^type_name>\<open>int\<close> @{thm perm_int_def}
+         |> discrete_fs_inst \<^type_name>\<open>int\<close> @{thm perm_int_def}
+         |> discrete_cp_inst \<^type_name>\<open>int\<close> @{thm perm_int_def}
+         |> discrete_pt_inst \<^type_name>\<open>char\<close> @{thm perm_char_def}
+         |> discrete_fs_inst \<^type_name>\<open>char\<close> @{thm perm_char_def}
+         |> discrete_cp_inst \<^type_name>\<open>char\<close> @{thm perm_char_def}
         end;
 
 
        (* abbreviations for some lemmas *)
        (*===============================*)

 
 
 (* syntax und parsing *)
 
 val _ =
-  Outer_Syntax.command @{command_keyword atom_decl} "declare new kinds of atoms"
+  Outer_Syntax.command \<^command_keyword>\<open>atom_decl\<close> "declare new kinds of atoms"
     (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
 
 end;