--- a/Nominal/nominal_function.ML Thu May 26 06:36:29 2011 +0200
+++ b/Nominal/nominal_function.ML Tue May 31 00:17:22 2011 +0100
@@ -140,7 +140,8 @@
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
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 *)
+ val (eqs, post, sort_cont, cnames) =
+ empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *)
val defname = mk_defname fixes
val FunctionConfig {partials, default, ...} = config