1.1 --- a/src/HOL/Induct/Comb.ML	Fri Aug 21 16:14:34 1998 +0200
     1.2 +++ b/src/HOL/Induct/Comb.ML	Fri Aug 21 17:49:21 1998 +0200
     1.3 @@ -29,16 +29,16 @@
     1.4  by (Blast_tac 1);
     1.5  by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
     1.6                            addSDs [spec_mp]) 1);
     1.7 -val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
     1.8 +qed_spec_mp "diamond_strip_lemmaE";
     1.9  
    1.10 -val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
    1.11 -by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
    1.12 +Goal "diamond(r) ==> diamond(r^*)";
    1.13 +by (stac diamond_def 1);  (*unfold only in goal, not in premise!*)
    1.14  by (rtac (impI RS allI RS allI) 1);
    1.15  by (etac rtrancl_induct 1);
    1.16  by (Blast_tac 1);
    1.17 -by (slow_best_tac  (*Seems to be a brittle, undirected search*)
    1.18 +by (best_tac  (*Seems to be a brittle, undirected search*)
    1.19      (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
    1.20 -            addEs [major RS diamond_strip_lemmaE]) 1);
    1.21 +            addEs [diamond_strip_lemmaE RS exE]) 1);
    1.22  qed "diamond_rtrancl";
    1.23  
    1.24