[isabelle] Case-combinator allows qualified names for bound variables

Referring to Isabelle-2014

Hi, I recently encountered the following (strange) behaviour:

theory Scratch
imports Main begin

    term "case a of Some Foo.bar ⇒ Foo.bar"

The term is accepted, and "Foo.bar" is highlighted as a bound variable. 

I would have expected that bound variables cannot have qualified names!?


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