diff -r 77e1d9f2925e -r c7d4bd9e89e0 Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Mon Jun 06 13:11:04 2011 +0100
+++ b/Nominal/nominal_function.ML	Tue Jun 07 08:52:59 2011 +0100
@@ -38,6 +38,7 @@
 struct
 
 open Function_Lib
+open Function_Common
 open Nominal_Function_Common