src/ZF/simpdata.ML

--- a/src/ZF/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -107,6 +107,6 @@
 
 simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
                            addsplits [split_if]
-                           setSolver Type_solver_tac;
+                           setSolver (mk_solver "types" Type_solver_tac);
 
 val ZF_ss = simpset();