Now uses thin_tac

--- a/src/ZF/OrderArith.ML	Thu Sep 05 18:30:13 1996 +0200
+++ b/src/ZF/OrderArith.ML	Thu Sep 05 18:31:14 1996 +0200
@@ -79,7 +79,7 @@
 by (rtac wf_onI2 1);
 by (subgoal_tac "ALL x:A. Inl(x): Ba" 1);
 (*Proving the lemma, which is needed twice!*)
-by (eres_inst_tac [("V", "y : A + B")] thin_rl 2);
+by (thin_tac "y : A + B" 2);
 by (rtac ballI 2);
 by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
 by (etac (bspec RS mp) 2);