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

[Brian Huffman]

On Fri, Nov 4, 2011 at 8:32 PM, Makarius <makarius at sketis.net> wrote:
> This syntax is only defined for single abstractions, but the categories got
> mixed up (the nonterminals via syntax types):
>
> syntax
>  "_lebesgue_integral" :: "'a => ('a => real) => ('a, 'b)
> measure_space_scheme => real"
>    ("\<integral> _. _ \<partial>_" [60,61] 110)
[..]
> The following should work better (cf. 5c760e1692b3):
>
> syntax
>  "_lebesgue_integral" :: "pttrn => real => ('a, 'b) measure_space_scheme =>
> real"
>    ("\<integral> _. _ \<partial>_" [60,61] 110)
>
> I.e. the slots for the concrete syntax are specified with the grammer in
> mind, not the resulting term after translation.  This can be also checked
> via 'print_syntax'.

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.
Even worse, this style makes it *look* like the types are checked,
which can be deceptive and confusing.

I would actually be in favor of changing the "syntax" command to
disallow logical types, requiring only nonterminal types to be used.

- Brian