# HG changeset patch
# User nipkow
# Date 833369657 -7200
# Node ID ee81183a77a00d2d26622af60332d139c489b9d1
# Parent  608050b43bee4914cf12b9a024a22549b7c51786
Replaced setsolver by addsolver

diff -r 608050b43bee -r ee81183a77a0 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Wed May 29 12:03:32 1996 +0200
+++ b/src/HOL/WF.ML	Wed May 29 13:34:17 1996 +0200
@@ -87,11 +87,10 @@
 
 (*** NOTE! some simplifications need a different finish_tac!! ***)
 fun indhyp_tac hyps =
-    resolve_tac (TrueI::refl::hyps) ORELSE' 
     (cut_facts_tac hyps THEN'
        DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
                         eresolve_tac [transD, mp, allE]));
-val wf_super_ss = HOL_ss setsolver indhyp_tac;
+val wf_super_ss = HOL_ss addsolver indhyp_tac;
 
 val prems = goalw WF.thy [is_recfun_def,cut_def]
     "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \