# HG changeset patch
# User lcp
# Date 782556878 -3600
# Node ID fb7345cccddc4628dcdad42d6208ee84563b4450
# Parent  7928c97606679b14192ce9a224acda3b6570606f
ZF/Fixedpt/coinduct: modified proof to suppress deep unification

diff -r 7928c9760667 -r fb7345cccddc src/ZF/Fixedpt.ML
--- 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();