--- a/src/HOL/SMT_Examples/SMT_Examples.thy Mon Mar 26 10:42:06 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Mon Mar 26 11:01:04 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 x = x \<and> id True = True" (* BROKEN by (smt id_def) *) oops
+lemma "id x = x \<and> id True = True" by (smt id_def)
lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
using fun_upd_same fun_upd_apply