src/ZF/equalities.ML

--- a/src/ZF/equalities.ML	Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/equalities.ML	Thu Jul 02 17:58:12 1998 +0200
@@ -601,7 +601,7 @@
 qed "Collect_Diff";
 
 goal ZF.thy "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
-by (simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (simp_tac (simpset() addsplits [split_if]) 1);
 by (Blast_tac 1);
 qed "Collect_cons";