src/HOL/WF.ML
changeset 1485 240cc98b94a7
parent 1475 7f5a4cd08209
child 1552 6f71b5d46700
     1.1 --- a/src/HOL/WF.ML	Fri Feb 09 12:18:02 1996 +0100
     1.2 +++ b/src/HOL/WF.ML	Fri Feb 09 13:41:18 1996 +0100
     1.3 @@ -100,8 +100,7 @@
     1.4  by (etac wf_induct 1);
     1.5  by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
     1.6  by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
     1.7 -qed "is_recfun_equal_lemma";
     1.8 -bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
     1.9 +qed_spec_mp "is_recfun_equal";
    1.10  
    1.11  
    1.12  val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
    1.13 @@ -191,7 +190,7 @@
    1.14  by (rtac refl 2);
    1.15  by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
    1.16  by (strip_tac 1);
    1.17 -by (res_inst_tac [("r2","r^+")] (is_recfun_equal_lemma RS mp RS mp) 1);
    1.18 +by (res_inst_tac [("r","r^+")] is_recfun_equal 1);
    1.19  by (atac 1);
    1.20  by (rtac trans_trancl 1);
    1.21  by (rtac unfold_the_recfun 1);