diff -r 8a98171ba1fc -r 93ab397f5980 Nominal/Perm.thy --- a/Nominal/Perm.thy Mon May 31 19:57:29 2010 +0200 +++ b/Nominal/Perm.thy Tue Jun 01 15:01:05 2010 +0200 @@ -5,9 +5,9 @@ "../Nominal-General/Nominal2_Eqvt" "Nominal2_FSet" "Abs" -(*uses ("nominal_dt_rawperm.ML") +uses ("nominal_dt_rawperm.ML") ("nominal_dt_rawfuns.ML") - ("nominal_dt_alpha.ML")*) + ("nominal_dt_alpha.ML") begin use "nominal_dt_rawperm.ML"