src/ZF/simpdata.ML

--- a/src/ZF/simpdata.ML	Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/simpdata.ML	Wed Dec 19 11:13:27 2001 +0100
@@ -104,8 +104,7 @@
 val Rep_simps = map prover
     ["{x. y:0, R(x,y)} = 0",	(*Replace*)
      "{x:0. P(x)} = 0",		(*Collect*)
-     "{x:A. False} = 0",
-     "{x:A. True} = A",
+     "{x:A. P} = (if P then A else 0)",
      "RepFun(0,f) = 0",		(*RepFun*)
      "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
      "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]