src/ZF/AC/Cardinal_aux.ML

--- a/src/ZF/AC/Cardinal_aux.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -69,7 +69,7 @@
                setloop (split_tac [expand_if] ORELSE' etac UnE);
 
 goal upair.thy "{x, y} - {y} = {x} - {y}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 val double_Diff_sing = result();
 
 goal upair.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";