removed duplicate type_solver (cf. Tools/typechk.ML);
--- 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