src/ZF/simpdata.ML

--- a/src/ZF/simpdata.ML	Mon Jul 13 16:42:27 1998 +0200
+++ b/src/ZF/simpdata.ML	Mon Jul 13 16:43:57 1998 +0200
@@ -104,6 +104,7 @@
 
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
-simpset_ref() := simpset() setmksimps (map mk_meta_eq o ZF_atomize o gen_all);
+simpset_ref() := simpset() setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
+                           addsplits [split_if];
 
 val ZF_ss = simpset();