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

[Makarius]

On Mon, 31 Oct 2011, Lars Noschinski wrote:

> I just noticed that the integral syntax defined in [1] can be used to trigger 
> some system-level exception: If, instead of the correct
>
>   \<integral> x. f x \<partial> y
>
> I write
>
>   \<integral> x x'. f x \<partial> y
>
> Isabelle prints
>
>   exception TERM raised (line 141 of "Syntax/syntax_trans.ML"): abs_tr

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)

Thus "x x'" was taken as application, not iterated identifiers in 
abstraction.


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'.


 	Makarius