# HG changeset patch
# User nipkow
# Date 823869787 -3600
# Node ID afc1c1f2523e252ffb8b813c43e62b0d751ce375
# Parent  7b95d7b49f7ade4e946e68a5b6b43a8721433103
replace sstac

diff -r 7b95d7b49f7a -r afc1c1f2523e src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Feb 09 13:41:59 1996 +0100
+++ b/src/HOL/ex/set.ML	Fri Feb 09 13:43:07 1996 +0100
@@ -89,7 +89,8 @@
 
 val [compl] = goal Lfp.thy
     "Compl(f``X) = g``Compl(X) ==> surj(%z. if z:X then f(z) else g(z))";
-by (sstac [surj_iff_full_range, range_if_then_else, compl RS sym] 1);
+by (EVERY1[stac surj_iff_full_range, stac range_if_then_else,
+           stac (compl RS sym)]);
 by (rtac (X_Un_Compl RS allI) 1);
 qed "surj_if_then_else";