[isabelle-dev] Abbreviations + Monad_Syntax introduce "unit itself" additional type variable

[Peter Lammich]

Referring to Isabelle_2013 AND Isabelle_12_Sep_2013:

In the following example, using an abbreviation that contains
monad-syntax introduces a superfluous additional itself-parameter, that,
however, is immediately instantiated to "unit itself". Note that, when
replacing abbreviation by definition, everything works as expected.

It looks like (see also my previous post) that monad-syntax has some
severe issues with abbreviations, that I would really like to see fixed
in the next release, as they render unusable many of my tools.

--
  Peter

theory Scratch
imports 
  "~~/src/HOL/Library/Monad_Syntax"
begin

abbreviation "abbr1 == Some () >>= (%_. Some False)"

abbreviation "abbr2 == do {
    Some ();
    Some False
  }"

(* ### Additional type variable(s) in specification of "abbr2": 'a *)

term "(abbr1, abbr2)"

(*
"(Some () >>= (%_::unit. Some False),
  %TYPE::unit itself. Some () >>= (%_::unit. Some False))"
  :: "bool option * (unit itself => bool option)"
*)


definition "abbr3 == do {
    Some ();
    Some False
  }"

(* No additional type parameter *)