diff -r 77e1d9f2925e -r c7d4bd9e89e0 Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Mon Jun 06 13:11:04 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Jun 07 08:52:59 2011 +0100
@@ -17,7 +17,7 @@
     -> term list
     -> local_theory
     -> ((thm (* goalstate *)
-        * (thm -> Nominal_Function_Common.function_result) (* proof continuation *)
+        * (thm -> Function_Common.function_result) (* proof continuation *)
        ) * local_theory)
 
 end
@@ -27,6 +27,7 @@
 struct
 
 open Function_Lib
+open Function_Common
 open Nominal_Function_Common
 
 type qgar = string * (string * typ) list * term list * term list * term