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