diff -r a9a1ed3f5023 -r 16b5a67ee279 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Jan 17 12:37:37 2011 +0000
+++ b/Nominal/Nominal2.thy	Mon Jan 17 14:37:18 2011 +0100
@@ -6,9 +6,11 @@
      ("nominal_dt_quot.ML")
      ("nominal_induct.ML")
      ("nominal_inductive.ML") 
+     ("nominal_function_core.ML")
+     ("nominal_mutual.ML")
+     ("nominal_function.ML")
 begin
 
-
 use "nominal_dt_rawfuns.ML"
 ML {* open Nominal_Dt_RawFuns *}
 
@@ -30,6 +32,13 @@
 use "nominal_inductive.ML" 
 
 
+(***************************************)
+(* forked code of the function package *)
+(* for defining nominal functions      *)
+use "nominal_function_core.ML"
+use "nominal_mutual.ML"
+use "nominal_function.ML"
+
 ML {*
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)