overloading of perm: adhoc name prevents duplicate fact names;

--- a/src/HOL/Nominal/nominal_package.ML	Mon Apr 14 17:54:56 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Apr 14 21:44:51 2008 +0200
@@ -300,7 +300,7 @@
     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))) |>
-      OldPrimrecPackage.add_primrec_unchecked_i "" perm_eqs;
+      OldPrimrecPackage.add_primrec_unchecked_i (serial_string ()) (* FIXME proper name *) perm_eqs;
 
     (**** prove that permutation functions introduced by unfolding are ****)
     (**** equivalent to already existing permutation functions         ****)