src/ZF/OrdQuant.ML

--- a/src/ZF/OrdQuant.ML	Thu Sep 24 17:16:06 1998 +0200
+++ b/src/ZF/OrdQuant.ML	Thu Sep 24 17:17:14 1998 +0200
@@ -98,7 +98,7 @@
 val Ord_atomize = atomize (("oall", [ospec])::ZF_conn_pairs, 
                            ZF_mem_pairs);
 
-simpset_ref() := simpset() setmksimps (map mk_meta_eq o Ord_atomize o gen_all)
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
                         addsimps [oall_simp, ltD RS beta]
                         addcongs [oall_cong, oex_cong, OUN_cong];