# HG changeset patch
# User haftmann
# Date 1372446461 -7200
# Node ID 9c7f760d06c2ec3dd1409493c216cc3a926c698e
# Parent  a2407f62a29fe77fc3ae2b99a218ab24463710df
formally accept dictionary parameters for constants on left hand sides in equations

diff -r a2407f62a29f -r 9c7f760d06c2 src/Tools/nbe.ML
--- 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';