adapted to latest change of Markus on the function package
authorChristian Urban <urbanc@in.tum.de>
Mon, 29 Oct 2012 14:00:48 +0000
changeset 3203 01a13904aaa5
parent 3202 3611bc56c177
child 3204 b69c8660de14
adapted to latest change of Markus on the function package
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