src/ZF/simpdata.ML

    ("op -",     [DiffD1,DiffD2]),
    ("op Int",   [IntD1,IntD2])];
 
 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
 
 val unfold_bex_tac = unfold_tac [Bex_def];
 fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;