--- a/src/ZF/simpdata.ML Fri Jul 30 10:44:34 2004 +0200
+++ b/src/ZF/simpdata.ML Fri Jul 30 10:44:42 2004 +0200
@@ -45,10 +45,13 @@
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));
+
simpset_ref() :=
simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
addcongs [if_weak_cong]
- setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));
+ setSolver type_solver;