diff -r fbbd65c89c23 -r 5324be24a5fa src/ZF/ex/Comb.ML
--- a/src/ZF/ex/Comb.ML	Fri Apr 26 13:30:26 1996 +0200
+++ b/src/ZF/ex/Comb.ML	Fri Apr 26 13:33:51 1996 +0200
@@ -177,9 +177,7 @@
 by (fast_tac (ZF_cs addIs [r_into_trancl]) 1);
 by (slow_best_tac (ZF_cs addSDs [spec RS mp]
                          addIs  [r_into_trancl, trans_trancl RS transD]) 1);
-qed "diamond_trancl_lemma";
-
-val diamond_lemmaE = diamond_trancl_lemma RS spec RS mp RS exE;
+val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
 
 val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)";
 by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
@@ -187,7 +185,7 @@
 by (etac trancl_induct 1);
 by (ALLGOALS
     (slow_best_tac (ZF_cs addIs [r_into_trancl, trans_trancl RS transD]
-                          addEs [major RS diamond_lemmaE])));
+                          addEs [major RS diamond_strip_lemmaE])));
 qed "diamond_trancl";