[isabelle] Strange eta-expanded "constants" in experiment environment

Hi List,

I ran into an odd effect: inside an experiment environment,
"definition" sometimes seems to produce (partially) eta-expanded terms
instead of constants! For me, it occurs in one of my own tools, and I
could not yet strip it down, but I found the same strange effect in the
standard "definition" command, when it automatically augments a type
argument. Outside an experiment environment, everything is as expected.

(minimal example attached)

What is going on here? To fix this thing for my tool, or strip it down
to a small example, I need some insights why this happens.

And another question: is this the expected behaviour of definition, to
generate an eta-expanded term instead of a constant? 

Also note that the pretty-printer seems not to be impressed by
[[eta_contract=false]] at all, and still prints the eta-contracted
version. (Which makes it even harder to figure out what is going on)

Thanks in advance for any pointers or explanations what is going on,


theory Scratch

  declare [[eta_contract = false]]


    definition "f ≡ length []" (* additional type var *)
    (* Looks OK *)
    term f (* "f" :: "'a itself ⇒ nat" *)
    (* But actually is an eta-expanded term, rather than a simple
constant: *)
    ML_val ‹@{term f}› (* Abs ("type", "'a itself", Const
("Scratch.experiment11092848.f", "'a itself ⇒ nat") $ Bound 0) *)

    (* And tools expecting constant fail on it *)
    ML_val ‹ @{const_name f}› (* Not a logical constant: "local.f" *)
    ML_val ‹ @{const f (nat)}› (* Not a logical constant: "local.f" *)

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