--- 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 *)