diff -r 77e1d9f2925e -r c7d4bd9e89e0 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Jun 06 13:11:04 2011 +0100
+++ b/Nominal/Nominal2.thy	Tue Jun 07 08:52:59 2011 +0100
@@ -6,7 +6,6 @@
      ("nominal_dt_quot.ML")
      ("nominal_induct.ML")
      ("nominal_inductive.ML")
-     ("nominal_function_common.ML")
      ("nominal_function_core.ML")
      ("nominal_mutual.ML")
      ("nominal_function.ML")
@@ -36,7 +35,6 @@
 (***************************************)
 (* 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"