--- a/src/ZF/OrderType.ML Wed Dec 14 16:57:55 1994 +0100
+++ b/src/ZF/OrderType.ML Wed Dec 14 17:15:54 1994 +0100
@@ -231,8 +231,8 @@
\ |] ==> R";
by (forward_tac [lt_eq_pred] 1);
be ltE 1;
-by (rtac (well_ord_Memrel RS not_well_ord_iso_pred RS notE) 1 THEN
- assume_tac 1 THEN assume_tac 1);
+by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
+ assume_tac 3 THEN assume_tac 1);
be subst 1;
by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1);
(*Combining the two simplifications causes looping*)