src/HOL/Lattices.thy

--- a/src/HOL/Lattices.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Lattices.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -291,7 +291,7 @@
 
 lemma (in linorder) distrib_lattice_min_max:
   "distrib_lattice (op \<le>) (op <) min max"
-proof unfold_locales
+proof
   have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
     by (auto simp add: less_le antisym)
   fix x y z