formally accept dictionary parameters for constants on left hand sides in equations

--- a/src/Tools/nbe.ML	Fri Jun 28 21:07:32 2013 +0200
+++ b/src/Tools/nbe.ML	Fri Jun 28 21:07:41 2013 +0200
@@ -356,7 +356,7 @@
         val default_rhs = nbe_apps_local (i+1) c (dicts @ default_args);
         val match_cont = if is_eval then NONE else SOME default_rhs;
         val assemble_arg = assemble_iterm
-          (fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts) NONE;
+          (fn c => fn dss => fn ts => nbe_apps_constr idx_of c ((maps o map) (K "_") dss @ ts)) NONE;
         val assemble_rhs = assemble_iterm assemble_constapp match_cont;
         val (samepairs, args') = subst_nonlin_vars args;
         val s_args = map assemble_arg args';