src/HOL/Set.thy

--- a/src/HOL/Set.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Set.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -1780,7 +1780,7 @@
   for f :: "'a::order \<Rightarrow> 'b::order"
   \<comment> \<open>Courtesy of Stephan Merz\<close>
   apply clarify
-  apply (erule_tac P = "\<lambda>x. x : S" in LeastI2_order)
+  apply (erule_tac P = "\<lambda>x. x \<in> S" in LeastI2_order)
    apply fast
   apply (rule LeastI2_order)
     apply (auto elim: monoD intro!: order_antisym)