--- a/Nominal/nominal_function_core.ML	Sun Jun 05 16:58:18 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Sun Jun 05 21:14:23 2011 +0100
@@ -11,14 +11,14 @@
 sig
   val trace: bool Unsynchronized.ref
 
-  val prepare_nominal_function : Function_Common.function_config
+  val prepare_nominal_function : Nominal_Function_Common.nominal_function_config
     -> string (* defname *)
     -> ((bstring * typ) * mixfix) list (* defined symbol *)
     -> ((bstring * typ) list * term list * term * term) list (* specification *)
     -> local_theory
     -> (term   (* f *)
         * thm  (* goalstate *)
-        * (thm -> Function_Common.function_result) (* continuation *)
+        * (thm -> Nominal_Function_Common.function_result) (* continuation *)
        ) * local_theory
 
 end
@@ -33,7 +33,7 @@
 val mk_eq = HOLogic.mk_eq
 
 open Function_Lib
-open Function_Common
+open Nominal_Function_Common
 
 datatype globals = Globals of
  {fvar: term,
@@ -905,7 +905,7 @@
 (* nominal *)
 fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
   let
-    val FunctionConfig {domintros, default=default_opt, ...} = config
+    val NominalFunctionConfig {domintros, default=default_opt, ...} = config
 
     val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
     val fvar = Free (fname, fT)