formally accept dictionary parameters for constants on left hand sides in equations
authorhaftmann
Fri Jun 28 21:07:41 2013 +0200 (2013-06-28)
changeset 524749c7f760d06c2
parent 52473 a2407f62a29f
child 52475 445ae7a4e4e1
formally accept dictionary parameters for constants on left hand sides in equations
src/Tools/nbe.ML
     1.1 --- a/src/Tools/nbe.ML	Fri Jun 28 21:07:32 2013 +0200
     1.2 +++ b/src/Tools/nbe.ML	Fri Jun 28 21:07:41 2013 +0200
     1.3 @@ -356,7 +356,7 @@
     1.4          val default_rhs = nbe_apps_local (i+1) c (dicts @ default_args);
     1.5          val match_cont = if is_eval then NONE else SOME default_rhs;
     1.6          val assemble_arg = assemble_iterm
     1.7 -          (fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts) NONE;
     1.8 +          (fn c => fn dss => fn ts => nbe_apps_constr idx_of c ((maps o map) (K "_") dss @ ts)) NONE;
     1.9          val assemble_rhs = assemble_iterm assemble_constapp match_cont;
    1.10          val (samepairs, args') = subst_nonlin_vars args;
    1.11          val s_args = map assemble_arg args';