author | berghofe |
Fri, 09 Jun 2006 17:32:38 +0200 | |
changeset 19834 | 2290cc06049b |
parent 19833 | 3a3f591c838d |
child 19835 | 81d6dc597559 |
--- 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 *} (*======================*)