--- a/src/ZF/OrderArith.ML Mon Sep 14 10:18:07 1998 +0200
+++ b/src/ZF/OrderArith.ML Tue Sep 15 10:40:40 1998 +0200
@@ -83,7 +83,7 @@
by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
by (best_tac (claset() addSEs [raddE, bspec RS mp]) 2);
(*Returning to main part of proof*)
-by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
+by Safe_tac;
by (Blast_tac 1);
by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
by (best_tac (claset() addSEs [raddE, bspec RS mp]) 1);