--- a/src/ZF/ROOT.ML Fri Jan 11 00:33:35 2002 +0100
+++ b/src/ZF/ROOT.ML Fri Jan 11 00:34:43 2002 +0100
@@ -22,7 +22,6 @@
use "~~/src/Provers/Arith/combine_numerals.ML";
with_path "Integ" use_thy "Main_ZFC";
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
print_depth 8;