[isabelle] Record updates on applications



Hi,

I have a question concerning concrete syntax for record updates. In
the context of a record R
  record R = f :: nat
I can write
  term "x(| f := 1 |)"
This gets displayed as
  "x(| f := 1 |)"
    :: "'a R_scheme"
which is what I'd expect. However, updating an application
  term "(g x)(| f := 1 |)"
gets displayed as
  "f_update (%_. 1) (g x)"
    :: "'a R_scheme"

I understand that both "g x"-terms are internally equal and that it's
just a matter of pretty printing. However, I don't understand why the
syntax translation machinery fails to pretty print the application.
Can somebody explain it to me?

Thanks,
  Dennis





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.