src/HOL/Nominal/nominal_atoms.ML
changeset 27691 ce171cbd4b93
parent 27399 1fb3d1219c12
child 28011 90074908db16
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 29 08:15:39 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 29 08:15:40 2008 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
     1.5        in
     1.6          thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
     1.7 -            |> PureThy.add_defs_unchecked_i true [((name, def2),[])]
     1.8 +            |> PureThy.add_defs_unchecked true [((name, def2),[])]
     1.9              |> snd
    1.10              |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
    1.11        end) ak_names_types thy1;
    1.12 @@ -207,7 +207,7 @@
    1.13            val def = Logic.mk_equals
    1.14                      (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
    1.15          in
    1.16 -          PureThy.add_defs_unchecked_i true [((name, def),[])] thy'
    1.17 +          PureThy.add_defs_unchecked true [((name, def),[])] thy'
    1.18          end) ak_names_types thy) ak_names_types thy4;
    1.19      
    1.20      (* proves that every atom-kind is an instance of at *)