src/ZF/simpdata.ML
changeset 279 7738aed3f84d
parent 14 1c0926788772
child 435 ca5356bd315a
--- a/src/ZF/simpdata.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/simpdata.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -86,9 +86,6 @@
       | _ $ A => tryrules atomize_pairs A
   end;
 
-fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
-
-
 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
 		beta, eta, restrict, fst_conv, snd_conv, split];
 
@@ -99,6 +96,6 @@
    [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
 
 val ZF_ss = FOL_ss 
-      setmksimps ZF_mk_rew_rules
+      setmksimps (map mk_meta_eq o atomize o gen_all)
       addsimps (ZF_simps @ mem_simps @ bquant_simps)
       addcongs ZF_congs;