[isabelle] Notation forgets unnamed context inside type class context



I have run into a problem with notation inside unnamed contexts in Isabelle2013-2 when the unnamed context is nested into a type class context. Suppose that the unnamed context fixes a parameter, locally define a constant that depends on the parameter and declare some mixfix notation for the constant inside the unnamed context. Then, the first place holder _ in the notation represents the parameter fixed in the unnamed context, rather than the first parameter of the locally defined constant.

Here's an example:

theory Scratch imports Main begin
context ord begin
context fixes f :: "'b => 'b" begin
definition foo :: "'b => 'b" where "foo x = f x"
notation (input) foo ("{|_|}")
term "{|undefined :: 'b|}" -- "type error in application"

If I do the same inside a proper locale instead of the type class context, notation works fine.

Moreover, I can refer to foo only via local.foo. If I write "foo", this always gets translated to the global foo with type "('c => 'c) => 'c => 'c".

Is there any way to use my notation in the unnamed context?

Best,
Andreas

PS: The same trouble occurs with a recent repository version such as 601ea66c5bcd.




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