added the hack "reset NameSpace.unique_names" to Nominal.thy
authorurbanc
Thu, 01 Jun 2006 14:15:08 +0200
changeset 19751 3006498da5c5
parent 19750 5281bd607206
child 19752 18e5aa65fb8b
added the hack "reset NameSpace.unique_names" to Nominal.thy (Stefan is working on a real fix in the nominal_package)
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 *}
 (*======================*)