--- a/src/HOL/SMT_Examples/SMT_Examples.thy Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Sun Mar 25 20:15:39 2012 +0200
@@ -467,7 +467,7 @@
lemma "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
by smt
-lemma "id 3 = 3 \<and> id True = True" by (smt id_def)
+lemma "id x = x \<and> id True = True" (* BROKEN by (smt id_def) *) oops
lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
using fun_upd_same fun_upd_apply