unique_names no longer set to false (thanks to improved naming
authorberghofe
Fri, 09 Jun 2006 17:32:38 +0200
changeset 19834 2290cc06049b
parent 19833 3a3f591c838d
child 19835 81d6dc597559
unique_names no longer set to false (thanks to improved naming scheme for "internal" constructors).
src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Jun 09 17:30:52 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Fri Jun 09 17:32:38 2006 +0200
@@ -9,9 +9,6 @@
   ("nominal_permeq.ML")
 begin 
 
-(* FIXME: this needs to be corrected in nominal_package *)
-ML {* reset NameSpace.unique_names; *}
-
 section {* Permutations *}
 (*======================*)