diff -r d1f7b6245a75 -r f5cafe803b55 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Jun 18 18:31:14 2009 -0700
+++ b/src/HOL/Nominal/Nominal.thy	Fri Jun 19 17:23:21 2009 +0200
@@ -3,7 +3,7 @@
 uses
   ("nominal_thmdecls.ML")
   ("nominal_atoms.ML")
-  ("nominal_package.ML")
+  ("nominal.ML")
   ("nominal_induct.ML") 
   ("nominal_permeq.ML")
   ("nominal_fresh_fun.ML")
@@ -3670,7 +3670,7 @@
 lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
   using assms ..
 
-use "nominal_package.ML"
+use "nominal.ML"
 
 (******************************************************)
 (* primitive recursive functions on nominal datatypes *)