src/ZF/simpdata.ML
changeset 12209 09bc6f8456b9
parent 12199 8213fd95acb5
child 12484 7ad150f5fc10
--- a/src/ZF/simpdata.ML	Thu Nov 15 18:20:48 2001 +0100
+++ b/src/ZF/simpdata.ML	Thu Nov 15 18:21:38 2001 +0100
@@ -45,10 +45,12 @@
 
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
-simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
-                           addcongs [if_weak_cong]
-		           addsplits [split_if]
-                           setSolver (mk_solver "types" Type_solver_tac);
+simpset_ref() :=
+  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
+  addcongs [if_weak_cong]
+  addsplits [split_if]
+  setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));
+
 
 (** Splitting IFs in the assumptions **)