[isabelle] HOL parser question



Hi,

for

 datatype A = c ("A")
 datatype B = B A

I get the following parser error:

*** Inner syntax error at: "A"
*** Expected tokens:  "_" "(" "[" "tvar" "tid" "longid" "id" "(|" "\<lparr>"
*** The error(s) above occurred in type "A"
*** The error above occured in constructor B of datatype B
*** At command "datatype".

however,

 datatype A = A
 datatype B = B A

or,

 datatype A = A ("c")
 datatype B = B A

is accepted.

Why this, is the name space for types and constants not separated?

Cheers Christian
theory D
imports Main
begin

datatype A = c ("A")
datatype B = B A

end


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