[isabelle-dev] implicit beta normalization in the pretty-printer

[Ondřej Kunčar]

Hi!
I found out that the pretty-printer for terms in Isabelle do implicitly 
beta-normalization and this behavior can't be turned off (in contrast to 
eta-normalization).

Is there any serious reason why I can't turn off this feature like in 
the case of eta-normalization? It's a bit annoying if you want to do 
debugging on the ML level and you have to inspect every term by 
inspecting its ML representation (which is really tedious for larger terms).

Thanks for an answer.
Ondrej