src/HOL/WF.ML
changeset 7570 a9391550eea1
parent 7499 23e090051cb8
child 8265 187cada50e19
     1.1 --- a/src/HOL/WF.ML	Tue Sep 21 19:10:39 1999 +0200
     1.2 +++ b/src/HOL/WF.ML	Tue Sep 21 19:11:07 1999 +0200
     1.3 @@ -260,7 +260,7 @@
     1.4      (cut_facts_tac hyps THEN'
     1.5         DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
     1.6                          eresolve_tac [transD, mp, allE]));
     1.7 -val wf_super_ss = HOL_ss addSolver indhyp_tac;
     1.8 +val wf_super_ss = HOL_ss addSolver (mk_solver "WF" indhyp_tac);
     1.9  
    1.10  Goalw [is_recfun_def,cut_def]
    1.11      "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \