[isabelle-dev] Mixfix-Syntax not recognized

[René Neumann]

Hi,

I'm currently on revision 8d8cb75ab20a, and mixfix-Syntax seems not
recognized in all cases (it seems like the syntax is only recognized if
the type is known, somewhat...).

Toy-Example (⇧ = \<^sup>) :

begin
definition foo :: "'a list ⇒ nat" ("(_⇧ω)") where
"foo xs = length xs"

term "foo xs" -- "type nat (as expected)"
term "xs⇧ω" -- "type 'a"
term "(xs::'a list)⇧ω" -- "type nat (as expected)"

lemma
  fixes xs :: "'a list" -- "learning, I explicitly fixed xs"
  shows "xs⇧ω = length xs" -- "but still does not recognize ω"
by (simp add: foo_def) -- "fails"
end

It works with Isabelle-2013, but already failed ~100 revisions ago in
-dev (unfortunately forgot to write the exact revision down).

It is probably related to the thread "Subscripts within identifiers",
but I'm not definitly sure.

Please just tell me, if I should test a couple more revisions

- René
-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4782 bytes
Desc: S/MIME Kryptografische Unterschrift
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130806/942cf7d9/attachment.p7s>