diff -r c7d4bd9e89e0 -r 23befefc6e73 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Tue Jun 07 08:52:59 2011 +0100
+++ b/Nominal/Nominal2.thy	Tue Jun 07 10:40:06 2011 +0100
@@ -6,6 +6,7 @@
      ("nominal_dt_quot.ML")
      ("nominal_induct.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"