--- a/src/ZF/Order.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Order.thy Mon Mar 23 21:05:17 2015 +0100
@@ -670,8 +670,8 @@
apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
apply blast
unfolding trans_on_def
- apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(?r).
- \<forall>z\<in>field(?r). \<langle>x, y\<rangle> \<in> ?r \<longrightarrow> \<langle>y, z\<rangle> \<in> ?r \<longrightarrow> \<langle>x, z\<rangle> \<in> ?r)" in rev_ballE)
+ apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(r).
+ \<forall>z\<in>field(r). \<langle>x, y\<rangle> \<in> r \<longrightarrow> \<langle>y, z\<rangle> \<in> r \<longrightarrow> \<langle>x, z\<rangle> \<in> r)" for r in rev_ballE)
(* instance obtained from proof term generated by best *)
apply best
apply blast