diff -r baeb0aeb4891 -r fb32b43e7f80 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Tue Jun 20 14:51:59 2006 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Tue Jun 20 15:53:44 2006 +0200
@@ -654,7 +654,7 @@
 lemma (in partial_order) total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   shows "total_order L"
-proof (rule total_order.intro)
+proof (intro_locales!)
   show "lattice_axioms L"
   proof (rule lattice_axioms.intro)
     fix x y
@@ -716,7 +716,7 @@
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "complete_lattice L"
-proof (rule complete_lattice.intro)
+proof (intro_locales!)
   show "lattice_axioms L"
     by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
 qed (assumption | rule complete_lattice_axioms.intro)+