changeset 19751 | 3006498da5c5 |
parent 19687 | 0a7c6d78ad6b |
child 19771 | b4a0da62126e |
--- 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 *} (*======================*)