diff -r 8fe80e9f796d -r 4bd584ff4fab Nominal/Nominal2.thy
--- 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"