unchecked definitions;

--- a/src/HOL/Nominal/nominal_atoms.ML	Sat May 13 02:51:47 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat May 13 02:51:48 2006 +0200
@@ -94,8 +94,8 @@
         val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
       in
         thy |> Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
-            |> (#2 o PureThy.add_defs_i true [((name, def2),[])])
-            |> PrimrecPackage.add_primrec_i "" [(("", def1),[])]            
+            |> (#2 o PureThy.add_defs_unchecked_i true [((name, def2),[])])
+            |> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]            
       end) (thy2, ak_names_types);
     
     (* declares a permutation function for every atom-kind acting  *)
@@ -123,7 +123,7 @@
                     Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
       in
         thy |> Theory.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
-            |> PrimrecPackage.add_primrec_i "" [(("", def1), []),(("", def2), [])]
+            |> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
       end) (thy3, ak_names_types);
     
     (* defines permutation functions for all combinations of atom-kinds; *)
@@ -148,7 +148,7 @@
           val def = Logic.mk_equals
                     (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
         in
-          PureThy.add_defs_i true [((name, def),[])] thy'
+          PureThy.add_defs_unchecked_i true [((name, def),[])] thy'
         end) ak_names_types thy) ak_names_types thy4;
     
     (* proves that every atom-kind is an instance of at *)

--- a/src/HOL/Nominal/nominal_package.ML	Sat May 13 02:51:47 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Sat May 13 02:51:48 2006 +0200
@@ -247,7 +247,7 @@
     val (thy2, perm_simps) = thy1 |>
       Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
         (List.drop (perm_names_types, length new_type_names))) |>
-      PrimrecPackage.add_primrec_i "" perm_eqs;
+      PrimrecPackage.add_primrec_unchecked_i "" perm_eqs;
 
     (**** prove that permutation functions introduced by unfolding are ****)
     (**** equivalent to already existing permutation functions         ****)
@@ -565,7 +565,7 @@
           val T = Type (Sign.intern_type thy name, tvs');
           val Const (_, Type (_, [U])) = c
         in apfst (pair r o hd)
-          (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
+          (PureThy.add_defs_unchecked_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
             (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
              Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
                (Const ("Nominal.perm", permT --> U --> U) $ pi $