# HG changeset patch
# User berghofe
# Date 1208371411 -7200
# Node ID 105031879f4a05b74dc9f37860ea6fae8d56f7d5
# Parent  6a91e368590da3b9d4d2a56cdb86ab1f2458a83d
Auxiliary permutation functions are no longer declared using add_consts_i,
because add_primrec_overloaded can do this as well.

diff -r 6a91e368590d -r 105031879f4a src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Apr 16 17:40:59 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Apr 16 20:43:31 2008 +0200
@@ -301,12 +301,11 @@
         end) constrs
       end) descr;
 
-    val (perm_simps, thy2) = thy1 |>
-      Sign.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
-        (List.drop (perm_names_types, length new_type_names))) |>
+    val (perm_simps, thy2) =
       PrimrecPackage.add_primrec_overloaded
-        (map2 (fn s => fn sT => (s, sT, false)) perm_names' perm_names_types)
-        (map (fn s => (s, NONE, NoSyn)) perm_names') perm_eqs;
+        (map (fn (s, sT) => (s, sT, false))
+           (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
+        (map (fn s => (s, NONE, NoSyn)) perm_names') perm_eqs thy1;
 
     (**** prove that permutation functions introduced by unfolding are ****)
     (**** equivalent to already existing permutation functions         ****)