--- a/src/HOL/Library/Order_Relation.thy Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Library/Order_Relation.thy Tue Nov 19 01:29:50 2013 +0100
@@ -93,7 +93,7 @@
using mono_Field[of "r - Id" r] Diff_subset[of r Id]
proof(auto)
have "r \<noteq> {}" using NID by fast
- then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by fast
+ then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto
hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
(* *)
fix a assume *: "a \<in> Field r"