ZF/Fixedpt/coinduct: modified proof to suppress deep unification

--- a/src/ZF/Fixedpt.ML	Wed Oct 19 09:48:13 1994 +0100
+++ b/src/ZF/Fixedpt.ML	Wed Oct 19 09:54:38 1994 +0100
@@ -275,7 +275,8 @@
 goal Fixedpt.thy
     "!!X D. [| bnd_mono(D,h);  a: X;  X <= h(X Un gfp(D,h));  X <= D |] ==> \
 \           a : gfp(D,h)";
-by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);
+by (rtac weak_coinduct 1);
+by (etac coinduct_lemma 2);
 by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1));
 val coinduct = result();