theory Scratch
  imports HOL.List
begin

declare [[ML_exception_debugger]]

lemma
  assumes "\<And>a. \<exists>!x. f x = [a]"
  shows "\<exists>!x. \<exists>!y. f x = [a] \<and> f y = [b]"
  using assms apply smt (* exception Option raised (line 82 of "General/basics.ML") *)
  oops

end