# HG changeset patch
# User wenzelm
# Date 1137880948 -3600
# Node ID f5fd06394f17a17e5f1ad36b6a56d60111916275
# Parent  f5ea6b0d35018d6c93a434c657429df788118b28
removed duplicate type_solver (cf. Tools/typechk.ML);

diff -r f5ea6b0d3501 -r f5fd06394f17 src/ZF/simpdata.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