# HG changeset patch
# User berghofe
# Date 1149867158 -7200
# Node ID 2290cc06049b4fde7341be8158bd8961b08c349d
# Parent  3a3f591c838dc744fcfc7dea73b9e81390468a18
unique_names no longer set to false (thanks to improved naming
scheme for "internal" constructors).

diff -r 3a3f591c838d -r 2290cc06049b 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 *}
 (*======================*)