src/ZF/Order.thy

--- a/src/ZF/Order.thy	Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/Order.thy	Fri May 24 13:15:37 2002 +0200
@@ -436,8 +436,7 @@
 apply (blast intro!: bij_converse_bij
              intro: bij_is_fun apply_funtype)+
 apply (erule notE)
-apply (simp add: left_inverse_bij bij_converse_bij bij_is_fun
-                 comp_fun_apply [of _ A B _ A])
+apply (simp add: left_inverse_bij bij_is_fun comp_fun_apply [of _ A B])
 done