[isabelle] Abbreviations in locales

Hi all,

I have a problem/question how abbreviations in locales are handled.
Regard the following toy example:

locale foo =
  fixes a :: 'a
  abbreviation "f == (a,a,a)"

locale bar1 = s1!: foo a for a
  term "s1.f" -- printed as s1.f

locale bar2 = s1!: foo b for b
  term "s1.f" -- printed as (b,b,b)

Why is the abbreviation in the second case valid input syntax, but not
pretty-printed in output? And how can I change this behaviour, towards
also using the abbreviation in the output?

A similar problem arises when interpreting the locales. 
After interpretation bar2 c (for constant c), the abbreviation "s1.f"
only works as input.

The current behaviour is somewhat strange, as it depends on the
conincidence of the parameter name in the locale expression 
"s1!: foo a for a" and the fixed variable name "a" that was used when
declaring the locale.

In my concrete example, I use quite a lot of abbreviations, and one gets
easily confused if one always sees them expanded in the output. Concrete
example: "s1.lookup" vs. "map_op_lookup ops1"

Thanks in advance for any help/hints 

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