src/HOL/WF.ML
changeset 2031 03a843f0f447
parent 1786 8a31d85d27b8
child 2637 e9b203f854ae
--- a/src/HOL/WF.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/WF.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -129,7 +129,7 @@
   by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
                    is_the_recfun 1);
   by (rewtac is_recfun_def);
-  by (rtac (cuts_eq RS ssubst) 1);
+  by (stac cuts_eq 1);
   by (rtac allI 1);
   by (rtac impI 1);
   by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1);
@@ -159,7 +159,7 @@
 by (wf_ind_tac "a" prems 1);
 by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); 
 by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
-by (rtac (cuts_eq RS ssubst) 1);
+by (stac cuts_eq 1);
 (*Applying the substitution: must keep the quantified assumption!!*)
 by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac,
             etac (mp RS ssubst), atac]);