[isabelle-dev] exception TERM raised (line 141 of "Syntax/syntax_trans.ML"): abs_tr
Makarius
makarius at sketis.net
Fri Nov 4 20:32:35 CET 2011
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
More information about the isabelle-dev
mailing list