src/ZF/Order.thy

 done
 
 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)
 done