[isabelle-dev] exception TERM raised (line 141 of "Syntax/syntax_trans.ML"): abs_tr

[Makarius]

On Fri, 4 Nov 2011, Brian Huffman wrote:

> Better yet, the "syntax" command probably ought to be used only with
> types containing nothing but nonterminals:
>
> syntax "_lebesgue_integral" :: "pttrn => logic => logic => logic"
>    ("\<integral> _. _ \<partial>_" [60,61] 110)
>
> Using any other kind of type expression with a "syntax" command is
> essentially a comment; such types are only used for generating
> nonterminals (type variables go to "any", type prop goes to "prop",
> other logical types go to "logic") and are not used for typechecking.

Such a non-conservative change always needs 2-3 good reasons for it and 
almost nothing against it -- to justify the effort required to get the 
implementation right and adapt existing applications.

I agree that "comments" are often deceptive, but the traditional idiom for 
Isabelle syntax uses the types exactly as such, to illustrate a little bit 
the intention of the notation.  (I have maintained all reachable syntax 
declarations for many years.) See e.g. 
http://isabelle.in.tum.de/repos/isabelle/file/5c760e1692b3/src/HOL/Isar_Examples/Hoare.thy#l191 
for an arbitrary example.  Even for a proper term constant the type scheme 
is just an approximation for the intended meaning.  For syntax the 
syntactic type does the same, although the type system happens to be 
slightly different.

Furthermore, asking users to write actual nonterminals exposes more 
technical details than necessary.  I never know myself on the spot where 
to put "logic" or "any" (it also depends on the LHS or RHS), and there are 
also "prop" vs. "prop'", for example.  I do know the system does it right 
when a certain standard idiom is followed.  (This is also what I did for 
5c760e1692b3, and used the "pttrn" stemming from existing practice, 
without delving into old questions about "pttrn" vs. "idt" again.)


 	Makarius