src/ZF/simpdata.ML
changeset 7570 a9391550eea1
parent 6153 bff90585cce5
child 9570 e16e168984e1
     1.1 --- a/src/ZF/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
     1.3 @@ -107,6 +107,6 @@
     1.4  
     1.5  simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
     1.6                             addsplits [split_if]
     1.7 -                           setSolver Type_solver_tac;
     1.8 +                           setSolver (mk_solver "types" Type_solver_tac);
     1.9  
    1.10  val ZF_ss = simpset();