diff -r 3611bc56c177 -r 01a13904aaa5 Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Fri Oct 19 09:40:24 2012 +0100
+++ b/Nominal/nominal_function.ML	Mon Oct 29 14:00:48 2012 +0000
@@ -142,7 +142,7 @@
     val fixes = map (apfst (apfst Binding.name_of)) fixes0;
     val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
     val (eqs, post, sort_cont, cnames) =  
-      empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *)
+      empty_preproc nominal_check_defs (Function_Common.default_config) ctxt' fixes spec (* nominal *)
 
     val defname = mk_defname fixes
     val NominalFunctionConfig {partials, ...} = config