diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/simpdata.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -95,7 +95,7 @@
 
 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
 		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff,
-		triv_RepFun];
+		triv_RepFun, subset_refl];
 
 (*Sigma_cong, Pi_cong NOT included by default since they cause
   flex-flex pairs and the "Check your prover" error -- because most