theory AmbiguousSyntaxBug
  imports Main
begin

(* introduce some overloaded notation *)
datatype o1 = O1 unit unit (infixr "?" 70)
datatype o2 = O2 unit unit (infixr "?" 70)

(* the following definition is accepted with a warning *)
fun ok :: "o1 \<Rightarrow> unit option \<Rightarrow> o2" where
  "ok (a ? b) (Some c) = () ? ()"

(* the following definitions produce errors *)
fun fail1 :: "o1 \<Rightarrow> unit option \<Rightarrow> unit" where
  "fail1 (a ? b) (Some _) = ()"

fun fail2 :: "o2 \<Rightarrow> unit option \<Rightarrow> unit" where
  "fail2 (a ? b) (Some _) = ()"

fun fail3 :: "unit option \<Rightarrow> o1" where
  "fail3 (Some _) = () ? ()"

fun fail4 :: "unit option \<Rightarrow> o2" where
  "fail4 (Some _) = () ? ()"

end