# HG changeset patch
# User wenzelm
# Date 1091177082 -7200
# Node ID 7fe7f022476cdb78eb34fa78b85c6240f252969e
# Parent  77d16046939022b3f2b6fe62c1dadf013ceac091
keep type_solver;

diff -r 77d160469390 -r 7fe7f022476c src/ZF/simpdata.ML
--- 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;