diff -r 055934ed89b0 -r 8f1e60d9f7cc src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Thu Feb 11 21:00:36 2010 +0100
+++ b/src/HOL/Lattices.thy	Mon Feb 15 01:27:06 2010 +0100
@@ -301,8 +301,7 @@
 
 lemma dual_bounded_lattice:
   "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
-  by (rule bounded_lattice.intro, rule dual_lattice)
-    (unfold_locales, auto simp add: less_le_not_le)
+  by unfold_locales (auto simp add: less_le_not_le)
 
 lemma inf_bot_left [simp]:
   "\<bottom> \<sqinter> x = \<bottom>"