diff -r db5026631799 -r a4476e55a241 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Mar 26 10:42:06 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Mar 26 11:01:04 2012 +0200
@@ -212,7 +212,7 @@
 lemma
   assumes "\<forall>x y. SMT.trigger [[SMT.pat (f x), SMT.pat (g y)]] (f x = g y)"
   shows "f a = g b"
-  using assms (* BROKEN by smt *) oops
+  using assms by smt
 
 lemma
   assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (P x --> Q x)"
@@ -853,7 +853,7 @@
   using point.simps
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt+ *) oops
+  by smt+
 
 lemma
   "cy (p \<lparr> cx := a \<rparr>) = cy p"
@@ -862,7 +862,7 @@
   using point.simps
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt+ *) oops
+  by smt+
 
 lemma
   "p1 = p2 \<longrightarrow> cx p1 = cx p2"
@@ -891,7 +891,7 @@
   using point.simps bw_point.simps
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt+ *) oops
+  by smt+
 
 lemma
   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
@@ -905,7 +905,7 @@
   using point.simps bw_point.simps
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt *) oops
+  by smt
 
 
 subsubsection {* Type definitions *}
@@ -919,7 +919,7 @@
   using n1_def n2_def n3_def nplus_def
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt+ *) oops
+  by smt+