Nominal/nominal_function.ML
changeset 2789 32979078bfe9
parent 2752 9f44608ea28d
child 2819 4bd584ff4fab
--- 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