changeset 18735 | f5fd06394f17 |
parent 18324 | d1c4b1112e33 |
child 24826 | 78e6a3cea367 |
--- a/src/ZF/simpdata.ML Sat Jan 21 23:02:27 2006 +0100 +++ b/src/ZF/simpdata.ML Sat Jan 21 23:02:28 2006 +0100 @@ -45,13 +45,9 @@ val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); -val type_solver = - mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)); - change_simpset (fn ss => ss setmksimps (map mk_eq o ZF_atomize o gen_all) - addcongs [if_weak_cong] - setSolver type_solver); + addcongs [if_weak_cong]); local