src/HOL/Set.thy

 lemma Least_mono:
   "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
     ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
     -- {* Courtesy of Stephan Merz *}
   apply clarify
-  apply (erule_tac P = "%x. x : S" in LeastI2, fast)
-  apply (rule LeastI2)
+  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
+  apply (rule LeastI2_order)
   apply (auto elim: monoD intro!: order_antisym)
   done
 
 
 subsection {* Inverse image of a function *}