diff -r 5079fdf938dd -r e329b36d9136 src/CCL/Gfp.ML
--- a/src/CCL/Gfp.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/Gfp.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -85,7 +85,7 @@
 by (rtac prem 1);
 by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1);
 by (rtac (mono RS monoD) 1);
-by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1);
+by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1);
 by (rtac Un_upper2 1);
 qed "coinduct3_lemma";