src/HOL/Nominal/nominal_atoms.ML
changeset 19635 f7aa7d174343
parent 19562 e56b3c967ae8
child 19638 4358b88a9d12
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat May 13 02:51:47 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat May 13 02:51:48 2006 +0200
     1.3 @@ -94,8 +94,8 @@
     1.4          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
     1.5        in
     1.6          thy |> Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
     1.7 -            |> (#2 o PureThy.add_defs_i true [((name, def2),[])])
     1.8 -            |> PrimrecPackage.add_primrec_i "" [(("", def1),[])]            
     1.9 +            |> (#2 o PureThy.add_defs_unchecked_i true [((name, def2),[])])
    1.10 +            |> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]            
    1.11        end) (thy2, ak_names_types);
    1.12      
    1.13      (* declares a permutation function for every atom-kind acting  *)
    1.14 @@ -123,7 +123,7 @@
    1.15                      Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
    1.16        in
    1.17          thy |> Theory.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
    1.18 -            |> PrimrecPackage.add_primrec_i "" [(("", def1), []),(("", def2), [])]
    1.19 +            |> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
    1.20        end) (thy3, ak_names_types);
    1.21      
    1.22      (* defines permutation functions for all combinations of atom-kinds; *)
    1.23 @@ -148,7 +148,7 @@
    1.24            val def = Logic.mk_equals
    1.25                      (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
    1.26          in
    1.27 -          PureThy.add_defs_i true [((name, def),[])] thy'
    1.28 +          PureThy.add_defs_unchecked_i true [((name, def),[])] thy'
    1.29          end) ak_names_types thy) ak_names_types thy4;
    1.30      
    1.31      (* proves that every atom-kind is an instance of at *)