src/ZF/Resid/SubUnion.ML

--- a/src/ZF/Resid/SubUnion.ML	Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/Resid/SubUnion.ML	Wed Nov 05 13:14:15 1997 +0100
@@ -120,7 +120,7 @@
     "!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_full_simp_tac
-             (simpset() setloop(SELECT_GOAL (safe_tac (claset()))))));
+             (simpset() setloop(SELECT_GOAL Safe_tac))));
 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
 by (Asm_full_simp_tac 1);
 qed_spec_mp "union_preserve_regular";