# HG changeset patch
# User paulson
# Date 841941074 -7200
# Node ID 58b60b558e48a4bf6fe3153836580134e37f2aa0
# Parent  589af052bcd46b49a5204e220fd6eb3cc200ec70
Now uses thin_tac

diff -r 589af052bcd4 -r 58b60b558e48 src/ZF/OrderArith.ML
--- 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);