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

[Lars Noschinski]

Hi all,

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

  -- Lars.

[1] src/HOL/Probability/Lebesgue_Integration.thy, lines 1688ff