diff -r 89d45187f04d -r ca5356bd315a src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/simpdata.ML	Tue Jun 21 17:20:34 1994 +0200
@@ -79,15 +79,18 @@
 		     Some rls => flat (map atomize ([th] RL rls))
 		   | None     => [th])
 	    | _ => [th]
-  in case concl_of th of (*The operator below is Trueprop*)
-	_ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b
-      | _ $ (Const("True",_)) => []	(*True is DELETED*)
-      | _ $ (Const("False",_)) => []	(*should False do something??*)
-      | _ $ A => tryrules atomize_pairs A
+  in case concl_of th of 
+       Const("Trueprop",_) $ P => 
+	  (case P of
+	       Const("op :",_) $ a $ b => tryrules atomize_mem_pairs b
+	     | Const("True",_)         => []
+	     | Const("False",_)        => []
+	     | A => tryrules atomize_pairs A)
+     | _                       => [th]
   end;
 
 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
-		beta, eta, restrict, fst_conv, snd_conv, split];
+		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff];
 
 (*Sigma_cong, Pi_cong NOT included by default since they cause
   flex-flex pairs and the "Check your prover" error -- because most