--- 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 |] ==> \