src/HOL/Nominal/nominal_atoms.ML
changeset 30345 76fd85bbf139
parent 30235 58d147683393
child 30595 c87a3350f5a9
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 07 22:16:50 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 07 22:17:25 2009 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4      
     1.5      val (_,thy1) = 
     1.6      fold_map (fn ak => fn thy => 
     1.7 -          let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) 
     1.8 +          let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
     1.9                val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
    1.10                val inject_flat = Library.flat inject
    1.11                val ak_type = Type (Sign.intern_type thy1 ak,[])
    1.12 @@ -187,7 +187,7 @@
    1.13                      cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
    1.14          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
    1.15        in
    1.16 -        thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
    1.17 +        thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)] 
    1.18              |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])]
    1.19              |> snd
    1.20              |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
    1.21 @@ -217,7 +217,7 @@
    1.22                     (Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
    1.23                      Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
    1.24        in
    1.25 -        thy |> Sign.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
    1.26 +        thy |> Sign.add_consts_i [(Binding.name prm_name, mk_permT T --> T --> T, NoSyn)] 
    1.27              |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
    1.28        end) ak_names_types thy3;
    1.29      
    1.30 @@ -300,7 +300,7 @@
    1.31                         (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
    1.32                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
    1.33        in
    1.34 -          AxClass.define_class (cl_name, ["HOL.type"]) []
    1.35 +          AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
    1.36                  [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
    1.37                   ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
    1.38                   ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
    1.39 @@ -349,7 +349,8 @@
    1.40            val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
    1.41  
    1.42         in  
    1.43 -        AxClass.define_class (cl_name, [pt_name]) [] [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy            
    1.44 +        AxClass.define_class (Binding.name cl_name, [pt_name]) []
    1.45 +          [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
    1.46         end) ak_names_types thy8; 
    1.47           
    1.48       (* proves that every fs_<ak>-type together with <ak>-type   *)
    1.49 @@ -398,7 +399,7 @@
    1.50                             (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
    1.51                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
    1.52                 in  
    1.53 -                 AxClass.define_class (cl_name, ["HOL.type"]) []
    1.54 +                 AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
    1.55                     [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'  
    1.56                 end) ak_names_types thy) ak_names_types thy12;
    1.57