more antiquotations;
authorwenzelm
Sat Mar 22 18:16:54 2014 +0100 (2014-03-22)
changeset 5625383b3c110f22d
parent 56252 b72e0a9d62b9
child 56254 a2dd9200854d
more antiquotations;
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 22 18:15:09 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 22 18:16:54 2014 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4  
     1.5  fun mk_Cons x xs =
     1.6    let val T = fastype_of x
     1.7 -  in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
     1.8 +  in Const (@{const_name Cons}, T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
     1.9  
    1.10  fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args);
    1.11  fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args);
    1.12 @@ -142,7 +142,7 @@
    1.13    
    1.14                val stmnt3 = HOLogic.mk_Trueprop
    1.15                             (HOLogic.mk_not
    1.16 -                              (Const ("Finite_Set.finite", HOLogic.mk_setT ak_type --> HOLogic.boolT) $
    1.17 +                              (Const (@{const_name finite}, HOLogic.mk_setT ak_type --> HOLogic.boolT) $
    1.18                                    HOLogic.mk_UNIV ak_type))
    1.19               
    1.20                val simp2 = [@{thm image_def},@{thm bex_UNIV}]@inject_thm
    1.21 @@ -179,9 +179,9 @@
    1.22          val b = Free ("b", T);
    1.23          val c = Free ("c", T);
    1.24          val ab = Free ("ab", HOLogic.mk_prodT (T, T))
    1.25 -        val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
    1.26 +        val cif = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
    1.27          val cswap_akname = Const (full_swap_name, swapT);
    1.28 -        val cswap = Const ("Nominal.swap", swapT)
    1.29 +        val cswap = Const (@{const_name Nominal.swap}, swapT)
    1.30  
    1.31          val name = swap_name ^ "_def";
    1.32          val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.33 @@ -215,7 +215,7 @@
    1.34          val xs = Free ("xs", mk_permT T);
    1.35          val a  = Free ("a", T) ;
    1.36  
    1.37 -        val cnil  = Const ("List.list.Nil", mk_permT T);
    1.38 +        val cnil  = Const (@{const_name Nil}, mk_permT T);
    1.39          
    1.40          val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (prm $ cnil $ a, a));
    1.41  
    1.42 @@ -245,7 +245,7 @@
    1.43            val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
    1.44            val pi = Free ("pi", mk_permT T);
    1.45            val a  = Free ("a", T');
    1.46 -          val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
    1.47 +          val cperm = Const (@{const_name Nominal.perm}, mk_permT T --> T' --> T');
    1.48            val thy'' = Sign.add_path "rec" thy'
    1.49            val cperm_def = Const (Sign.full_bname thy'' perm_def_name, mk_permT T --> T' --> T');
    1.50            val thy''' = Sign.parent_path thy'';
    1.51 @@ -265,7 +265,7 @@
    1.52        let
    1.53          val ak_name_qu = Sign.full_bname thy5 (ak_name);
    1.54          val i_type = Type(ak_name_qu,[]);
    1.55 -        val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
    1.56 +        val cat = Const (@{const_name Nominal.at}, Term.itselfT i_type --> HOLogic.boolT);
    1.57          val at_type = Logic.mk_type i_type;
    1.58          fun proof ctxt =
    1.59            simp_tac (put_simpset HOL_ss ctxt
    1.60 @@ -290,14 +290,14 @@
    1.61       val (pt_ax_classes,thy7) =  fold_map (fn (ak_name, T) => fn thy =>
    1.62        let 
    1.63            val cl_name = "pt_"^ak_name;
    1.64 -          val ty = TFree("'a",["HOL.type"]);
    1.65 +          val ty = TFree("'a", @{sort type});
    1.66            val x   = Free ("x", ty);
    1.67            val pi1 = Free ("pi1", mk_permT T);
    1.68            val pi2 = Free ("pi2", mk_permT T);
    1.69 -          val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
    1.70 -          val cnil  = Const ("List.list.Nil", mk_permT T);
    1.71 -          val cappend = Const ("List.append",mk_permT T --> mk_permT T --> mk_permT T);
    1.72 -          val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
    1.73 +          val cperm = Const (@{const_name Nominal.perm}, mk_permT T --> ty --> ty);
    1.74 +          val cnil  = Const (@{const_name Nil}, mk_permT T);
    1.75 +          val cappend = Const (@{const_name append}, mk_permT T --> mk_permT T --> mk_permT T);
    1.76 +          val cprm_eq = Const (@{const_name Nominal.prm_eq}, mk_permT T --> mk_permT T --> HOLogic.boolT);
    1.77            (* nil axiom *)
    1.78            val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
    1.79                         (cperm $ cnil $ x, x));
    1.80 @@ -309,7 +309,7 @@
    1.81                         (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
    1.82                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
    1.83        in
    1.84 -          Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
    1.85 +          Axclass.define_class (Binding.name cl_name, @{sort type}) []
    1.86                  [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
    1.87                   ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
    1.88                   ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
    1.89 @@ -326,7 +326,8 @@
    1.90          val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name);
    1.91          val i_type1 = TFree("'x",[pt_name_qu]);
    1.92          val i_type2 = Type(ak_name_qu,[]);
    1.93 -        val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.94 +        val cpt =
    1.95 +          Const (@{const_name Nominal.pt}, (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.96          val pt_type = Logic.mk_type i_type1;
    1.97          val at_type = Logic.mk_type i_type2;
    1.98          fun proof ctxt =
    1.99 @@ -349,10 +350,10 @@
   1.100         let 
   1.101            val cl_name = "fs_"^ak_name;
   1.102            val pt_name = Sign.full_bname thy ("pt_"^ak_name);
   1.103 -          val ty = TFree("'a",["HOL.type"]);
   1.104 +          val ty = TFree("'a",@{sort type});
   1.105            val x   = Free ("x", ty);
   1.106 -          val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
   1.107 -          val cfinite  = Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT)
   1.108 +          val csupp    = Const (@{const_name Nominal.supp}, ty --> HOLogic.mk_setT T);
   1.109 +          val cfinite  = Const (@{const_name finite}, HOLogic.mk_setT T --> HOLogic.boolT)
   1.110            
   1.111            val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
   1.112  
   1.113 @@ -372,7 +373,7 @@
   1.114           val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name);
   1.115           val i_type1 = TFree("'x",[fs_name_qu]);
   1.116           val i_type2 = Type(ak_name_qu,[]);
   1.117 -         val cfs = Const ("Nominal.fs", 
   1.118 +         val cfs = Const (@{const_name Nominal.fs},
   1.119                                   (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   1.120           val fs_type = Logic.mk_type i_type1;
   1.121           val at_type = Logic.mk_type i_type2;
   1.122 @@ -394,19 +395,19 @@
   1.123           fold_map (fn (ak_name', T') => fn thy' =>
   1.124               let
   1.125                 val cl_name = "cp_"^ak_name^"_"^ak_name';
   1.126 -               val ty = TFree("'a",["HOL.type"]);
   1.127 +               val ty = TFree("'a",@{sort type});
   1.128                 val x   = Free ("x", ty);
   1.129                 val pi1 = Free ("pi1", mk_permT T);
   1.130                 val pi2 = Free ("pi2", mk_permT T');                  
   1.131 -               val cperm1 = Const ("Nominal.perm", mk_permT T  --> ty --> ty);
   1.132 -               val cperm2 = Const ("Nominal.perm", mk_permT T' --> ty --> ty);
   1.133 -               val cperm3 = Const ("Nominal.perm", mk_permT T  --> mk_permT T' --> mk_permT T');
   1.134 +               val cperm1 = Const (@{const_name Nominal.perm}, mk_permT T  --> ty --> ty);
   1.135 +               val cperm2 = Const (@{const_name Nominal.perm}, mk_permT T' --> ty --> ty);
   1.136 +               val cperm3 = Const (@{const_name Nominal.perm}, mk_permT T  --> mk_permT T' --> mk_permT T');
   1.137  
   1.138                 val ax1   = HOLogic.mk_Trueprop 
   1.139                             (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
   1.140                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
   1.141                 in  
   1.142 -                 Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
   1.143 +                 Axclass.define_class (Binding.name cl_name, @{sort type}) []
   1.144                     [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'  
   1.145                 end) ak_names_types thy) ak_names_types thy12;
   1.146  
   1.147 @@ -422,7 +423,7 @@
   1.148               val i_type0 = TFree("'a",[cp_name_qu]);
   1.149               val i_type1 = Type(ak_name_qu,[]);
   1.150               val i_type2 = Type(ak_name_qu',[]);
   1.151 -             val ccp = Const ("Nominal.cp",
   1.152 +             val ccp = Const (@{const_name Nominal.cp},
   1.153                               (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
   1.154                                                        (Term.itselfT i_type2)-->HOLogic.boolT);
   1.155               val at_type  = Logic.mk_type i_type1;
   1.156 @@ -456,7 +457,7 @@
   1.157                   val ak_name_qu' = Sign.full_bname thy' ak_name';
   1.158                   val i_type1 = Type(ak_name_qu,[]);
   1.159                   val i_type2 = Type(ak_name_qu',[]);
   1.160 -                 val cdj = Const ("Nominal.disjoint",
   1.161 +                 val cdj = Const (@{const_name Nominal.disjoint},
   1.162                             (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   1.163                   val at_type  = Logic.mk_type i_type1;
   1.164                   val at_type' = Logic.mk_type i_type2;
   1.165 @@ -548,15 +549,14 @@
   1.166            val pt_thm_unit  = pt_unit_inst;
   1.167         in
   1.168          thy
   1.169 -        |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
   1.170 -        |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
   1.171 -        |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
   1.172 -        |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
   1.173 -        |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
   1.174 -        |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
   1.175 -        |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   1.176 -                                    (pt_proof pt_thm_nprod)
   1.177 -        |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
   1.178 +        |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
   1.179 +        |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
   1.180 +        |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
   1.181 +        |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
   1.182 +        |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
   1.183 +        |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
   1.184 +        |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_nprod)
   1.185 +        |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (pt_proof pt_thm_unit)
   1.186       end) ak_names thy13; 
   1.187  
   1.188         (********  fs_<ak> class instances  ********)
   1.189 @@ -614,12 +614,11 @@
   1.190            val fs_thm_optn  = fs_inst RS fs_option_inst;
   1.191          in 
   1.192           thy
   1.193 -         |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
   1.194 -         |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
   1.195 -         |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   1.196 -                                     (fs_proof fs_thm_nprod) 
   1.197 -         |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
   1.198 -         |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
   1.199 +         |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (fs_proof fs_thm_unit) 
   1.200 +         |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
   1.201 +         |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_nprod)
   1.202 +         |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
   1.203 +         |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
   1.204          end) ak_names thy20;
   1.205  
   1.206         (********  cp_<ak>_<ai> class instances  ********)
   1.207 @@ -698,13 +697,13 @@
   1.208              val cp_thm_set = cp_inst RS cp_set_inst;
   1.209          in
   1.210           thy'
   1.211 -         |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
   1.212 +         |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (cp_proof cp_thm_unit)
   1.213           |> Axclass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   1.214 -         |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   1.215 -         |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   1.216 -         |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   1.217 -         |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   1.218 -         |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
   1.219 +         |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   1.220 +         |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   1.221 +         |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   1.222 +         |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   1.223 +         |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
   1.224          end) ak_names thy) ak_names thy25;
   1.225  
   1.226       (* show that discrete nominal types are permutation types, finitely     *)
     2.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 22 18:15:09 2014 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 22 18:16:54 2014 +0100
     2.3 @@ -90,13 +90,14 @@
     2.4  
     2.5  val dj_cp = @{thm dj_cp};
     2.6  
     2.7 -fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
     2.8 -      Type ("fun", [_, U])])) = (T, U);
     2.9 +fun dest_permT (Type (@{type_name fun},
    2.10 +    [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [T, _])]),
    2.11 +      Type (@{type_name fun}, [_, U])])) = (T, U);
    2.12  
    2.13 -fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
    2.14 +fun permTs_of (Const (@{const_name Nominal.perm}, T) $ t $ u) = fst (dest_permT T) :: permTs_of u
    2.15    | permTs_of _ = [];
    2.16  
    2.17 -fun perm_simproc' ctxt (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
    2.18 +fun perm_simproc' ctxt (Const (@{const_name Nominal.perm}, T) $ t $ (u as Const (@{const_name Nominal.perm}, U) $ r $ s)) =
    2.19        let
    2.20          val thy = Proof_Context.theory_of ctxt;
    2.21          val (aT as Type (a, []), S) = dest_permT T;
    2.22 @@ -140,23 +141,23 @@
    2.23    let
    2.24      val T = fastype_of1 (Ts, t);
    2.25      val U = fastype_of1 (Ts, u)
    2.26 -  in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
    2.27 +  in Const (@{const_name Nominal.perm}, T --> U --> U) $ t $ u end;
    2.28  
    2.29  fun perm_of_pair (x, y) =
    2.30    let
    2.31      val T = fastype_of x;
    2.32      val pT = mk_permT T
    2.33 -  in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
    2.34 -    HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
    2.35 +  in Const (@{const_name Cons}, HOLogic.mk_prodT (T, T) --> pT --> pT) $
    2.36 +    HOLogic.mk_prod (x, y) $ Const (@{const_name Nil}, pT)
    2.37    end;
    2.38  
    2.39  fun mk_not_sym ths = maps (fn th => case prop_of th of
    2.40      _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
    2.41    | _ => [th]) ths;
    2.42  
    2.43 -fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
    2.44 +fun fresh_const T U = Const (@{const_name Nominal.fresh}, T --> U --> HOLogic.boolT);
    2.45  fun fresh_star_const T U =
    2.46 -  Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
    2.47 +  Const (@{const_name Nominal.fresh_star}, HOLogic.mk_setT T --> U --> HOLogic.boolT);
    2.48  
    2.49  fun gen_nominal_datatype prep_specs config dts thy =
    2.50    let
    2.51 @@ -185,8 +186,8 @@
    2.52        (Sign.full_name thy n, Sign.full_name thy (Binding.suffix_name "_Rep" n))) dts;
    2.53      val rps = map Library.swap ps;
    2.54  
    2.55 -    fun replace_types (Type ("Nominal.ABS", [T, U])) =
    2.56 -          Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
    2.57 +    fun replace_types (Type (@{type_name ABS}, [T, U])) =
    2.58 +          Type (@{type_name fun}, [T, Type (@{type_name noption}, [replace_types U])])
    2.59        | replace_types (Type (s, Ts)) =
    2.60            Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
    2.61        | replace_types T = T;
    2.62 @@ -208,14 +209,14 @@
    2.63  
    2.64      (**** define permutation functions ****)
    2.65  
    2.66 -    val permT = mk_permT (TFree ("'x", HOLogic.typeS));
    2.67 +    val permT = mk_permT (TFree ("'x", @{sort type}));
    2.68      val pi = Free ("pi", permT);
    2.69      val perm_types = map (fn (i, _) =>
    2.70        let val T = nth_dtyp i
    2.71        in permT --> T --> T end) descr;
    2.72      val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
    2.73        "perm_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr);
    2.74 -    val perm_names = replicate (length new_type_names) "Nominal.perm" @
    2.75 +    val perm_names = replicate (length new_type_names) @{const_name Nominal.perm} @
    2.76        map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
    2.77      val perm_names_types = perm_names ~~ perm_types;
    2.78      val perm_names_types' = perm_names' ~~ perm_types;
    2.79 @@ -236,16 +237,16 @@
    2.80                    fold_rev (Term.abs o pair "x") Us
    2.81                      (Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
    2.82                        list_comb (x, map (fn (i, U) =>
    2.83 -                        Const ("Nominal.perm", permT --> U --> U) $
    2.84 -                          (Const ("List.rev", permT --> permT) $ pi) $
    2.85 +                        Const (@{const_name Nominal.perm}, permT --> U --> U) $
    2.86 +                          (Const (@{const_name rev}, permT --> permT) $ pi) $
    2.87                            Bound i) ((length Us - 1 downto 0) ~~ Us)))
    2.88                  end
    2.89 -              else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
    2.90 +              else Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x
    2.91              end;
    2.92          in
    2.93            (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
    2.94              (Free (nth perm_names_types' i) $
    2.95 -               Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
    2.96 +               Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
    2.97                 list_comb (c, args),
    2.98               list_comb (c, map perm_arg (dts ~~ args)))))
    2.99          end) constrs
   2.100 @@ -274,7 +275,7 @@
   2.101              (map (fn (c as (s, T), x) =>
   2.102                 let val [T1, T2] = binder_types T
   2.103                 in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
   2.104 -                 Const ("Nominal.perm", T) $ pi $ Free (x, T2))
   2.105 +                 Const (@{const_name Nominal.perm}, T) $ pi $ Free (x, T2))
   2.106                 end)
   2.107               (perm_names_types ~~ perm_indnames))))
   2.108            (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
   2.109 @@ -293,7 +294,7 @@
   2.110              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   2.111                (map (fn ((s, T), x) => HOLogic.mk_eq
   2.112                    (Const (s, permT --> T --> T) $
   2.113 -                     Const ("List.list.Nil", permT) $ Free (x, T),
   2.114 +                     Const (@{const_name Nil}, permT) $ Free (x, T),
   2.115                     Free (x, T)))
   2.116                 (perm_names ~~
   2.117                  map body_type perm_types ~~ perm_indnames)))))
   2.118 @@ -326,7 +327,7 @@
   2.119                  (map (fn ((s, T), x) =>
   2.120                      let val perm = Const (s, permT --> T --> T)
   2.121                      in HOLogic.mk_eq
   2.122 -                      (perm $ (Const ("List.append", permT --> permT --> permT) $
   2.123 +                      (perm $ (Const (@{const_name append}, permT --> permT --> permT) $
   2.124                           pi1 $ pi2) $ Free (x, T),
   2.125                         perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
   2.126                      end)
   2.127 @@ -357,7 +358,7 @@
   2.128        in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm
   2.129          (Goal.prove_global_future thy2 [] []
   2.130            (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
   2.131 -             (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
   2.132 +             (HOLogic.mk_Trueprop (Const (@{const_name Nominal.prm_eq},
   2.133                  permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
   2.134                HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   2.135                  (map (fn ((s, T), x) =>
   2.136 @@ -414,7 +415,7 @@
   2.137                      val pi2 = Free ("pi2", permT2);
   2.138                      val perm1 = Const (s, permT1 --> T --> T);
   2.139                      val perm2 = Const (s, permT2 --> T --> T);
   2.140 -                    val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
   2.141 +                    val perm3 = Const (@{const_name Nominal.perm}, permT1 --> permT2 --> permT2)
   2.142                    in HOLogic.mk_eq
   2.143                      (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
   2.144                       perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
   2.145 @@ -462,17 +463,17 @@
   2.146          (map (fn (i, _) => Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr);
   2.147      val big_rep_name =
   2.148        space_implode "_" (Datatype_Prop.indexify_names (map_filter
   2.149 -        (fn (i, ("Nominal.noption", _, _)) => NONE
   2.150 +        (fn (i, (@{type_name noption}, _, _)) => NONE
   2.151            | (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
   2.152      val _ = warning ("big_rep_name: " ^ big_rep_name);
   2.153  
   2.154      fun strip_option (dtf as Datatype.DtType ("fun", [dt, Datatype.DtRec i])) =
   2.155            (case AList.lookup op = descr i of
   2.156 -             SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
   2.157 +             SOME (@{type_name noption}, _, [(_, [dt']), _]) =>
   2.158                 apfst (cons dt) (strip_option dt')
   2.159             | _ => ([], dtf))
   2.160        | strip_option (Datatype.DtType ("fun",
   2.161 -            [dt, Datatype.DtType ("Nominal.noption", [dt'])])) =
   2.162 +            [dt, Datatype.DtType (@{type_name noption}, [dt'])])) =
   2.163            apfst (cons dt) (strip_option dt')
   2.164        | strip_option dt = ([], dt);
   2.165  
   2.166 @@ -493,8 +494,8 @@
   2.167              val free' = Datatype_Aux.app_bnds free (length Us);
   2.168              fun mk_abs_fun T (i, t) =
   2.169                let val U = fastype_of t
   2.170 -              in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
   2.171 -                Type ("Nominal.noption", [U])) $ Datatype_Aux.mk_Free "y" T i $ t)
   2.172 +              in (i + 1, Const (@{const_name Nominal.abs_fun}, [T, U, T] --->
   2.173 +                Type (@{type_name noption}, [U])) $ Datatype_Aux.mk_Free "y" T i $ t)
   2.174                end
   2.175            in (j + 1, j' + length Ts,
   2.176              case dt'' of
   2.177 @@ -513,7 +514,7 @@
   2.178  
   2.179      val (intr_ts, (rep_set_names', recTs')) =
   2.180        apfst flat (apsnd ListPair.unzip (ListPair.unzip (map_filter
   2.181 -        (fn ((_, ("Nominal.noption", _, _)), _) => NONE
   2.182 +        (fn ((_, (@{type_name noption}, _, _)), _) => NONE
   2.183            | ((i, (_, _, constrs)), rep_set_name) =>
   2.184                let val T = nth_dtyp i
   2.185                in SOME (map (make_intr rep_set_name T) constrs,
   2.186 @@ -540,7 +541,7 @@
   2.187      val abs_perm = Global_Theory.get_thms thy4 "abs_perm";
   2.188  
   2.189      val perm_indnames' = map_filter
   2.190 -      (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
   2.191 +      (fn (x, (_, (@{type_name noption}, _, _))) => NONE | (x, _) => SOME x)
   2.192        (perm_indnames ~~ descr);
   2.193  
   2.194      fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp))
   2.195 @@ -553,7 +554,7 @@
   2.196                   val S = Const (s, T --> HOLogic.boolT);
   2.197                   val permT = mk_permT (Type (name, []))
   2.198                 in HOLogic.mk_imp (S $ Free (x, T),
   2.199 -                 S $ (Const ("Nominal.perm", permT --> T --> T) $
   2.200 +                 S $ (Const (@{const_name Nominal.perm}, permT --> T --> T) $
   2.201                     Free ("pi", permT) $ Free (x, T)))
   2.202                 end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
   2.203          (fn {context = ctxt, ...} => EVERY
   2.204 @@ -581,15 +582,15 @@
   2.205                (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
   2.206          let
   2.207            val permT = mk_permT
   2.208 -            (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
   2.209 +            (TFree (singleton (Name.variant_list (map fst tvs)) "'a", @{sort type}));
   2.210            val pi = Free ("pi", permT);
   2.211            val T = Type (Sign.full_name thy name, map TFree tvs);
   2.212          in apfst (pair r o hd)
   2.213            (Global_Theory.add_defs_unchecked true
   2.214              [((Binding.map_name (fn n => "prm_" ^ n ^ "_def") name, Logic.mk_equals
   2.215 -              (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
   2.216 +              (Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ Free ("x", T),
   2.217                 Const (Sign.intern_const thy ("Abs_" ^ Binding.name_of name), U --> T) $
   2.218 -                 (Const ("Nominal.perm", permT --> U --> U) $ pi $
   2.219 +                 (Const (@{const_name Nominal.perm}, permT --> U --> U) $ pi $
   2.220                     (Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $
   2.221                       Free ("x", T))))), [])] thy)
   2.222          end))
   2.223 @@ -671,12 +672,12 @@
   2.224          val T = fastype_of x;
   2.225          val U = fastype_of t
   2.226        in
   2.227 -        Const ("Nominal.abs_fun", T --> U --> T -->
   2.228 -          Type ("Nominal.noption", [U])) $ x $ t
   2.229 +        Const (@{const_name Nominal.abs_fun}, T --> U --> T -->
   2.230 +          Type (@{type_name noption}, [U])) $ x $ t
   2.231        end;
   2.232  
   2.233      val (ty_idxs, _) = List.foldl
   2.234 -      (fn ((i, ("Nominal.noption", _, _)), p) => p
   2.235 +      (fn ((i, (@{type_name noption}, _, _)), p) => p
   2.236          | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
   2.237  
   2.238      fun reindex (Datatype.DtType (s, dts)) = Datatype.DtType (s, map reindex dts)
   2.239 @@ -691,7 +692,7 @@
   2.240        in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
   2.241  
   2.242      val (descr'', ndescr) = ListPair.unzip (map_filter
   2.243 -      (fn (i, ("Nominal.noption", _, _)) => NONE
   2.244 +      (fn (i, (@{type_name noption}, _, _)) => NONE
   2.245          | (i, (s, dts, constrs)) =>
   2.246               let
   2.247                 val SOME index = AList.lookup op = ty_idxs i;
   2.248 @@ -817,8 +818,8 @@
   2.249            (augment_sort thy8
   2.250              (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
   2.251              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   2.252 -              (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
   2.253 -               Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
   2.254 +              (Const (@{const_name Nominal.perm}, permT --> U --> U) $ pi $ (Rep $ x),
   2.255 +               Rep $ (Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x)))))
   2.256            (fn {context = ctxt, ...} =>
   2.257              simp_tac (put_simpset HOL_basic_ss ctxt addsimps (perm_defs @ Abs_inverse_thms @
   2.258              perm_closed_thms @ Rep_thms)) 1)
   2.259 @@ -860,7 +861,7 @@
   2.260  
   2.261            fun perm t =
   2.262              let val T = fastype_of t
   2.263 -            in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
   2.264 +            in Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ t end;
   2.265  
   2.266            fun constr_arg (dts, dt) (j, l_args, r_args) =
   2.267              let
   2.268 @@ -977,7 +978,7 @@
   2.269            val Ts = map fastype_of args1;
   2.270            val c = list_comb (Const (cname, Ts ---> T), args1);
   2.271            fun supp t =
   2.272 -            Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
   2.273 +            Const (@{const_name Nominal.supp}, fastype_of t --> HOLogic.mk_setT atomT) $ t;
   2.274            fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
   2.275            val supp_thm = Goal.prove_global_future thy8 [] []
   2.276              (augment_sort thy8 pt_cp_sort
   2.277 @@ -1070,8 +1071,8 @@
   2.278             (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
   2.279               (HOLogic.mk_Trueprop
   2.280                 (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
   2.281 -                 Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
   2.282 -                   (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
   2.283 +                 Const (@{const_name finite}, HOLogic.mk_setT atomT --> HOLogic.boolT) $
   2.284 +                   (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT atomT) $ Free (s, T)))
   2.285                     (indnames ~~ recTs)))))
   2.286             (fn {context = ctxt, ...} => Datatype_Aux.ind_tac dt_induct indnames 1 THEN
   2.287              ALLGOALS (asm_full_simp_tac (ctxt addsimps
   2.288 @@ -1112,10 +1113,10 @@
   2.289  
   2.290      val pnames = if length descr'' = 1 then ["P"]
   2.291        else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
   2.292 -    val ind_sort = if null dt_atomTs then HOLogic.typeS
   2.293 +    val ind_sort = if null dt_atomTs then @{sort type}
   2.294        else Sign.minimize_sort thy9 (Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms));
   2.295      val fsT = TFree ("'n", ind_sort);
   2.296 -    val fsT' = TFree ("'n", HOLogic.typeS);
   2.297 +    val fsT' = TFree ("'n", @{sort type});
   2.298  
   2.299      val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
   2.300        (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
   2.301 @@ -1183,7 +1184,7 @@
   2.302  
   2.303      val ind_prems' =
   2.304        map (fn (_, f as Free (_, T)) => Logic.all (Free ("x", fsT'))
   2.305 -        (HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
   2.306 +        (HOLogic.mk_Trueprop (Const (@{const_name finite},
   2.307            Term.range_type T -->
   2.308              HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
   2.309        maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
   2.310 @@ -1345,7 +1346,7 @@
   2.311                            cut_facts_tac iprems 1,
   2.312                            (resolve_tac prems THEN_ALL_NEW
   2.313                              SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
   2.314 -                                _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
   2.315 +                                _ $ (Const (@{const_name Nominal.fresh}, _) $ _ $ _) =>
   2.316                                    simp_tac ind_ss1' i
   2.317                                | _ $ (Const (@{const_name Not}, _) $ _) =>
   2.318                                    resolve_tac freshs2' i
   2.319 @@ -1371,7 +1372,7 @@
   2.320        map (fn (_, f) =>
   2.321          let val f' = Logic.varify_global f
   2.322          in (cterm_of thy9 f',
   2.323 -          cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
   2.324 +          cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f')))
   2.325          end) fresh_fs) induct_aux;
   2.326  
   2.327      val induct = Goal.prove_global_future thy9 []
   2.328 @@ -1398,7 +1399,7 @@
   2.329  
   2.330      val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' used;
   2.331  
   2.332 -    val rec_sort = if null dt_atomTs then HOLogic.typeS else
   2.333 +    val rec_sort = if null dt_atomTs then @{sort type} else
   2.334        Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
   2.335  
   2.336      val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
   2.337 @@ -1459,8 +1460,8 @@
   2.338            HOLogic.mk_Trueprop (nth rec_preds i $ Free y)) (recs ~~ frees'');
   2.339          val prems5 = mk_fresh3 (recs ~~ frees'') frees';
   2.340          val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
   2.341 -          (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
   2.342 -             (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
   2.343 +          (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
   2.344 +             (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT aT) $ Free y)))
   2.345                 frees'') atomTs;
   2.346          val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
   2.347            (fresh_const T fsT' $ Free x $ rec_ctxt)) binders;
   2.348 @@ -1534,7 +1535,7 @@
   2.349                (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
   2.350              (fn {context = ctxt, ...} => dtac (Thm.instantiate ([],
   2.351                   [(cterm_of thy11 (Var (("pi", 0), permT)),
   2.352 -                   cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
   2.353 +                   cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN
   2.354                 NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths)
   2.355        in (ths, ths') end) dt_atomTs);
   2.356  
   2.357 @@ -1545,9 +1546,9 @@
   2.358          val name = Long_Name.base_name (fst (dest_Type aT));
   2.359          val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
   2.360          val aset = HOLogic.mk_setT aT;
   2.361 -        val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
   2.362 +        val finite = Const (@{const_name finite}, aset --> HOLogic.boolT);
   2.363          val fins = map (fn (f, T) => HOLogic.mk_Trueprop
   2.364 -          (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
   2.365 +          (finite $ (Const (@{const_name Nominal.supp}, T --> aset) $ f)))
   2.366              (rec_fns ~~ rec_fn_Ts)
   2.367        in
   2.368          map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm
   2.369 @@ -1561,7 +1562,7 @@
   2.370                       val y = Free ("y" ^ string_of_int i, U)
   2.371                     in
   2.372                       HOLogic.mk_imp (R $ x $ y,
   2.373 -                       finite $ (Const ("Nominal.supp", U --> aset) $ y))
   2.374 +                       finite $ (Const (@{const_name Nominal.supp}, U --> aset) $ y))
   2.375                     end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~
   2.376                       (1 upto length recTs))))))
   2.377              (fn {prems = fins, context = ctxt} =>
   2.378 @@ -1573,8 +1574,8 @@
   2.379  
   2.380      val finite_premss = map (fn aT =>
   2.381        map (fn (f, T) => HOLogic.mk_Trueprop
   2.382 -        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
   2.383 -           (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
   2.384 +        (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
   2.385 +           (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT aT) $ f)))
   2.386             (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
   2.387  
   2.388      val rec_fns' = map (augment_sort thy11 fs_cp_sort) rec_fns;
   2.389 @@ -1613,7 +1614,7 @@
   2.390                   in EVERY
   2.391                     [rtac (Drule.cterm_instantiate
   2.392                        [(cterm_of thy11 S,
   2.393 -                        cterm_of thy11 (Const ("Nominal.supp",
   2.394 +                        cterm_of thy11 (Const (@{const_name Nominal.supp},
   2.395                            fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
   2.396                        supports_fresh) 1,
   2.397                      simp_tac (put_simpset HOL_basic_ss context addsimps
   2.398 @@ -1654,7 +1655,7 @@
   2.399      val induct_aux_rec = Drule.cterm_instantiate
   2.400        (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
   2.401           (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT,
   2.402 -            Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
   2.403 +            Const (@{const_name Nominal.supp}, fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
   2.404                fresh_fs @
   2.405            map (fn (((P, T), (x, U)), Q) =>
   2.406             (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
   2.407 @@ -1684,8 +1685,8 @@
   2.408  
   2.409      val finite_ctxt_prems = map (fn aT =>
   2.410        HOLogic.mk_Trueprop
   2.411 -        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
   2.412 -           (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
   2.413 +        (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
   2.414 +           (Const (@{const_name Nominal.supp}, fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
   2.415  
   2.416      val rec_unique_thms = Datatype_Aux.split_conj_thm (Goal.prove
   2.417        (Proof_Context.init_global thy11) (map fst rec_unique_frees)
   2.418 @@ -1752,7 +1753,7 @@
   2.419                          | _ => false)
   2.420                        | _ => false) prems';
   2.421                      val fresh_prems = filter (fn th => case prop_of th of
   2.422 -                        _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
   2.423 +                        _ $ (Const (@{const_name Nominal.fresh}, _) $ _ $ _) => true
   2.424                        | _ $ (Const (@{const_name Not}, _) $ _) => true
   2.425                        | _ => false) prems';
   2.426                      val Ts = map fastype_of boundsl;
     3.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Mar 22 18:15:09 2014 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Mar 22 18:16:54 2014 +0100
     3.3 @@ -87,8 +87,8 @@
     3.4    | get_inner_fresh_fun (v as Var _)  = NONE
     3.5    | get_inner_fresh_fun (Const _) = NONE
     3.6    | get_inner_fresh_fun (Abs (_, _, t)) = get_inner_fresh_fun t
     3.7 -  | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u)
     3.8 -                           = SOME T
     3.9 +  | get_inner_fresh_fun (Const (@{const_name Nominal.fresh_fun},
    3.10 +      Type(@{type_name fun},[Type (@{type_name fun},[Type (T,_),_]),_])) $ u) = SOME T
    3.11    | get_inner_fresh_fun (t $ u) =
    3.12       let val a = get_inner_fresh_fun u in
    3.13       if a = NONE then get_inner_fresh_fun t else a
     4.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Mar 22 18:15:09 2014 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Mar 22 18:16:54 2014 +0100
     4.3 @@ -196,7 +196,7 @@
     4.4        end) (Logic.strip_imp_prems raw_induct' ~~ avoids');
     4.5  
     4.6      val atomTs = distinct op = (maps (map snd o #2) prems);
     4.7 -    val ind_sort = if null atomTs then HOLogic.typeS
     4.8 +    val ind_sort = if null atomTs then @{sort type}
     4.9        else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
    4.10          ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
    4.11      val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
    4.12 @@ -332,7 +332,7 @@
    4.13                   fun concat_perm pi1 pi2 =
    4.14                     let val T = fastype_of pi1
    4.15                     in if T = fastype_of pi2 then
    4.16 -                       Const (@{const_name List.append}, T --> T --> T) $ pi1 $ pi2
    4.17 +                       Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
    4.18                       else pi2
    4.19                     end;
    4.20                   val pis'' = fold (concat_perm #> map) pis' pis;
     5.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 22 18:15:09 2014 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 22 18:16:54 2014 +0100
     5.3 @@ -45,7 +45,7 @@
     5.4  
     5.5  fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
     5.6    (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
     5.7 -    fn Const ("Nominal.perm", _) $ _ $ t =>
     5.8 +    fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
     5.9           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    5.10           then SOME perm_bool else NONE
    5.11       | _ => NONE);
    5.12 @@ -97,13 +97,13 @@
    5.13        (case head_of p of
    5.14           Const (name, _) =>
    5.15             if member (op =) names name then SOME (HOLogic.mk_conj (p,
    5.16 -             Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
    5.17 +             Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
    5.18                 (subst_bounds (pis, strip_all pis q))))
    5.19             else NONE
    5.20         | _ => NONE)
    5.21    | inst_conj_all names ps pis t u =
    5.22        if member (op aconv) ps (head_of u) then
    5.23 -        SOME (Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
    5.24 +        SOME (Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
    5.25            (subst_bounds (pis, strip_all pis t)))
    5.26        else NONE
    5.27    | inst_conj_all _ _ _ _ _ = NONE;
    5.28 @@ -222,7 +222,7 @@
    5.29  
    5.30      val atomTs = distinct op = (maps (map snd o #2) prems);
    5.31      val atoms = map (fst o dest_Type) atomTs;
    5.32 -    val ind_sort = if null atomTs then HOLogic.typeS
    5.33 +    val ind_sort = if null atomTs then @{sort type}
    5.34        else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
    5.35          ("fs_" ^ Long_Name.base_name a)) atoms));
    5.36      val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
    5.37 @@ -292,7 +292,7 @@
    5.38        ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
    5.39      val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
    5.40        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    5.41 -      addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    5.42 +      addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
    5.43          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
    5.44      val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
    5.45      val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
    5.46 @@ -312,7 +312,7 @@
    5.47          (** protect terms to avoid that fresh_star_prod_set interferes with  **)
    5.48          (** pairs used in introduction rules of inductive predicate          **)
    5.49          fun protect t =
    5.50 -          let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end;
    5.51 +          let val T = fastype_of t in Const (@{const_name Fun.id}, T --> T) $ t end;
    5.52          val p = foldr1 HOLogic.mk_prod (map protect ts);
    5.53          val atom = fst (dest_Type T);
    5.54          val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
    5.55 @@ -393,7 +393,7 @@
    5.56                   fun concat_perm pi1 pi2 =
    5.57                     let val T = fastype_of pi1
    5.58                     in if T = fastype_of pi2 then
    5.59 -                       Const ("List.append", T --> T --> T) $ pi1 $ pi2
    5.60 +                       Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
    5.61                       else pi2
    5.62                     end;
    5.63                   val pis'' = fold_rev (concat_perm #> map) pis' pis;
     6.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Mar 22 18:15:09 2014 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Mar 22 18:16:54 2014 +0100
     6.3 @@ -97,14 +97,15 @@
     6.4      (* constant or when (f x) is a permuation with two or more arguments     *)
     6.5      fun applicable_app t = 
     6.6            (case (strip_comb t) of
     6.7 -              (Const ("Nominal.perm",_),ts) => (length ts) >= 2
     6.8 +              (Const (@{const_name Nominal.perm},_),ts) => (length ts) >= 2
     6.9              | (Const _,_) => false
    6.10              | _ => true)
    6.11    in
    6.12      case redex of 
    6.13          (* case pi o (f x) == (pi o f) (pi o x)          *)
    6.14 -        (Const("Nominal.perm",
    6.15 -          Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
    6.16 +        (Const(@{const_name Nominal.perm},
    6.17 +          Type(@{type_name fun},
    6.18 +            [Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
    6.19              (if (applicable_app f) then
    6.20                let
    6.21                  val name = Long_Name.base_name n
    6.22 @@ -124,13 +125,13 @@
    6.23       fun applicable_fun t =
    6.24         (case (strip_comb t) of
    6.25            (Abs _ ,[]) => true
    6.26 -        | (Const ("Nominal.perm",_),_) => false
    6.27 +        | (Const (@{const_name Nominal.perm},_),_) => false
    6.28          | (Const _, _) => true
    6.29          | _ => false)
    6.30     in
    6.31       case redex of 
    6.32         (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
    6.33 -       (Const("Nominal.perm",_) $ pi $ f)  => 
    6.34 +       (Const(@{const_name Nominal.perm},_) $ pi $ f)  => 
    6.35            (if applicable_fun f then SOME perm_fun_def else NONE)
    6.36        | _ => NONE
    6.37     end
    6.38 @@ -190,9 +191,9 @@
    6.39  
    6.40  fun perm_compose_simproc' ctxt redex =
    6.41    (case redex of
    6.42 -     (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
    6.43 -       [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
    6.44 -         Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ 
    6.45 +     (Const (@{const_name Nominal.perm}, Type (@{type_name fun}, [Type (@{type_name list},
    6.46 +       [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm}, 
    6.47 +         Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ 
    6.48            pi2 $ t)) =>
    6.49      let
    6.50        val thy = Proof_Context.theory_of ctxt
    6.51 @@ -293,7 +294,7 @@
    6.52      let val goal = nth (cprems_of st) (i - 1)
    6.53      in
    6.54        case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
    6.55 -          _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
    6.56 +          _ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) =>
    6.57            let
    6.58              val cert = Thm.cterm_of (Thm.theory_of_thm st);
    6.59              val ps = Logic.strip_params (term_of goal);
    6.60 @@ -303,7 +304,7 @@
    6.61                  HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
    6.62                vs HOLogic.unit;
    6.63              val s' = fold_rev Term.abs ps
    6.64 -              (Const ("Nominal.supp", fastype_of1 (Ts, s) -->
    6.65 +              (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) -->
    6.66                  Term.range_type T) $ s);
    6.67              val supports_rule' = Thm.lift_rule goal supports_rule;
    6.68              val _ $ (_ $ S $ _) =
    6.69 @@ -337,7 +338,7 @@
    6.70          val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
    6.71      in
    6.72        case Logic.strip_assums_concl (term_of goal) of
    6.73 -          _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 
    6.74 +          _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) => 
    6.75            let
    6.76              val cert = Thm.cterm_of (Thm.theory_of_thm st);
    6.77              val ps = Logic.strip_params (term_of goal);
    6.78 @@ -348,7 +349,7 @@
    6.79                vs HOLogic.unit;
    6.80              val s' =
    6.81                fold_rev Term.abs ps
    6.82 -                (Const ("Nominal.supp", fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
    6.83 +                (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
    6.84              val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
    6.85              val _ $ (_ $ S $ _) =
    6.86                Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));