src/HOL/WF.ML
changeset 1771 ee81183a77a0
parent 1760 6f41a494f3b1
child 1786 8a31d85d27b8
--- 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 |] ==> \