# HG changeset patch
# User urbanc
# Date 1149164108 -7200
# Node ID 3006498da5c53ec21047dbf1687365dc07cfa012
# Parent  5281bd607206276ecadf9ba78a45656e5b431a32
added the hack "reset NameSpace.unique_names" to Nominal.thy
(Stefan is working on a real fix in the nominal_package)

diff -r 5281bd607206 -r 3006498da5c5 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue May 30 12:24:04 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu Jun 01 14:15:08 2006 +0200
@@ -9,6 +9,9 @@
   ("nominal_permeq.ML")
 begin 
 
+(* FIXME: this needs to be corrected in nominal_package *)
+ML {* reset NameSpace.unique_names; *}
+
 section {* Permutations *}
 (*======================*)