src/ZF/Order.ML

--- a/src/ZF/Order.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/Order.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -496,7 +496,7 @@
 \                     range(ord_iso_map(A,r,B,s)), s)";
 by (asm_simp_tac (simpset() addsimps [ord_iso_map_fun]) 1);
 by Safe_tac;
-by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1);
+by (subgoals_tac ["x:A", "ya:A", "y:B", "yb:B"] 1);
 by (REPEAT 
     (blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
 by (asm_simp_tac