src/ZF/simpdata.ML
changeset 12725 7ede865e1fe5
parent 12720 f8a134b9a57f
child 12825 f1f7964ed05c
     1.1 --- a/src/ZF/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
     1.2 +++ b/src/ZF/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
     1.5  
     1.6  simpset_ref() :=
     1.7 -  simpset() setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
     1.8 +  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
     1.9    addcongs [if_weak_cong]
    1.10    addsplits [split_if]
    1.11    setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));