src/ZF/ROOT.ML

--- a/src/ZF/ROOT.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/ROOT.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -44,6 +44,8 @@
 (*the all-in-one theory*)
 use_thy "Main";
 
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
+
 print_depth 8;
 
 Goal "True";  (*leave subgoal package empty*)