src/ZF/WF.ML
changeset 7570 a9391550eea1
parent 6112 5e4871c5136b
child 9173 422968aeed49
     1.1 --- a/src/ZF/WF.ML	Tue Sep 21 19:10:39 1999 +0200
     1.2 +++ b/src/ZF/WF.ML	Tue Sep 21 19:11:07 1999 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4                          eresolve_tac [underD, transD, spec RS mp]));
     1.5  
     1.6  (*** NOTE! some simplifications need a different solver!! ***)
     1.7 -val wf_super_ss = simpset() setSolver indhyp_tac;
     1.8 +val wf_super_ss = simpset() setSolver (mk_solver "WF" indhyp_tac);
     1.9  
    1.10  Goalw [is_recfun_def]
    1.11      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \