src/ZF/OrdQuant.ML
changeset 12725 7ede865e1fe5
parent 12720 f8a134b9a57f
     1.1 --- a/src/ZF/OrdQuant.ML	Fri Jan 11 18:49:25 2002 +0100
     1.2 +++ b/src/ZF/OrdQuant.ML	Sat Jan 12 16:37:58 2002 +0100
     1.3 @@ -103,7 +103,7 @@
     1.4  
     1.5  val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
     1.6  
     1.7 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe)
     1.8 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
     1.9                          addsimps [oall_simp, ltD RS beta]
    1.10                          addcongs [oall_cong, oex_cong, OUN_cong];
    1.11