diff -r 5079fdf938dd -r e329b36d9136 src/CCL/coinduction.ML
--- a/src/CCL/coinduction.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/coinduction.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -7,7 +7,7 @@
 *)
 
 val [mono,prem] = goal Lfp.thy "[| mono(f);  a : f(lfp(f)) |] ==> a : lfp(f)";
-by (rtac ((mono RS lfp_Tarski) RS ssubst) 1);
+by (stac (mono RS lfp_Tarski) 1);
 by (rtac prem 1);
 qed "lfpI";