# HG changeset patch
# User wenzelm
# Date 1208202291 -7200
# Node ID 540ad65e804c266e45a179fb0f548106009f1e4c
# Parent  e114be97befe58e143d8bf887f4ea16c6119fcb3
overloading of perm: adhoc name prevents duplicate fact names;

diff -r e114be97befe -r 540ad65e804c src/HOL/Nominal/nominal_package.ML
--- 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         ****)