# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1351519248 0
# Node ID 01a13904aaa51bb300b17208507a5902076b5e4e
# Parent  3611bc56c177994af9c561d8bf535400e570b3dc
adapted to latest change of Markus on the function package

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