diff -r 8fe80e9f796d -r 4bd584ff4fab Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Sun Jun 05 16:58:18 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Sun Jun 05 21:14:23 2011 +0100
@@ -11,13 +11,13 @@
 signature NOMINAL_FUNCTION_MUTUAL =
 sig
 
-  val prepare_nominal_function_mutual : Function_Common.function_config
+  val prepare_nominal_function_mutual : Nominal_Function_Common.nominal_function_config
     -> string (* defname *)
     -> ((string * typ) * mixfix) list
     -> term list
     -> local_theory
     -> ((thm (* goalstate *)
-        * (thm -> Function_Common.function_result) (* proof continuation *)
+        * (thm -> Nominal_Function_Common.function_result) (* proof continuation *)
        ) * local_theory)
 
 end
@@ -27,7 +27,7 @@
 struct
 
 open Function_Lib
-open Function_Common
+open Nominal_Function_Common
 
 type qgar = string * (string * typ) list * term list * term list * term