Isabelle exception

THM0_741.thy

theory THM0_741 imports Main begin

datatype 'a s  = S 'a

datatype 'a t = T ‹'a s›

primrec f :: ‹'a s ⇒ 'a set› where
  ‹f (S x) = {x}›

primrec g :: ‹'a t ⇒ 'a set› where
  ‹g (T x) = f x›

lemma trigger: ‹f t ⊆ UNIV›
  by blast

lemma ‹g p ⊆ UNIV›
  using trigger (* raises: *)
proof (induct p)
  case (T x)    (* exception THM 0 raised (line 741 of "thm.ML"): assume: variables *)
  then show ?case
    by simp
qed

end