--- a/src/ZF/Order.thy Wed Jul 10 16:07:52 2002 +0200
+++ b/src/ZF/Order.thy Wed Jul 10 16:54:07 2002 +0200
@@ -321,7 +321,7 @@
lemma linear_ord_iso:
"[| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)"
apply (simp add: linear_def ord_iso_def, safe)
-apply (drule_tac x1 = "f`x" and x = "f`xa" in bspec [THEN bspec])
+apply (drule_tac x1 = "f`x" and x = "f`y" in bspec [THEN bspec])
apply (safe elim!: bij_is_fun [THEN apply_type])
apply (drule_tac t = "op ` (converse (f))" in subst_context)
apply (simp add: left_inverse_bij)