src/HOL/Lattices_Big.thy

--- a/src/HOL/Lattices_Big.thy	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/HOL/Lattices_Big.thy	Fri Mar 14 10:08:36 2014 +0100
@@ -640,6 +640,11 @@
   shows "Max M \<le> Max N"
   using assms by (fact Max.antimono)
 
+end
+
+context linorder  (* FIXME *)
+begin
+
 lemma mono_Min_commute:
   assumes "mono f"
   assumes "finite A" and "A \<noteq> {}"