--- a/Nominal/Nominal2.thy Sun Jun 05 16:58:18 2011 +0100
+++ b/Nominal/Nominal2.thy Sun Jun 05 21:14:23 2011 +0100
@@ -5,7 +5,8 @@
("nominal_dt_alpha.ML")
("nominal_dt_quot.ML")
("nominal_induct.ML")
- ("nominal_inductive.ML")
+ ("nominal_inductive.ML")
+ ("nominal_function_common.ML")
("nominal_function_core.ML")
("nominal_mutual.ML")
("nominal_function.ML")
@@ -35,6 +36,7 @@
(***************************************)
(* forked code of the function package *)
(* for defining nominal functions *)
+use "nominal_function_common.ML"
use "nominal_function_core.ML"
use "nominal_mutual.ML"
use "nominal_function.ML"