diff -r 036a19936feb -r 32979078bfe9 Nominal/nominal_function.ML --- 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