src/ZF/Main.ML

--- a/src/ZF/Main.ML	Fri Jan 11 00:33:35 2002 +0100
+++ b/src/ZF/Main.ML	Fri Jan 11 00:34:43 2002 +0100
@@ -3,3 +3,5 @@
 struct
   val thy = the_context ();
 end;
+
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);