src/HOL/Induct/Comb.thy

--- a/src/HOL/Induct/Comb.thy	Tue Jun 28 15:27:45 2005 +0200
+++ b/src/HOL/Induct/Comb.thy	Tue Jun 28 15:28:04 2005 +0200
@@ -104,8 +104,7 @@
 apply (simp (no_asm_simp) add: diamond_def)
 apply (rule impI [THEN allI, THEN allI])
 apply (erule rtrancl_induct, blast)
-apply (best intro: rtrancl_trans [OF _ r_into_rtrancl] 
-            elim: diamond_strip_lemmaE [THEN exE])
+apply (meson rtrancl_trans r_into_rtrancl diamond_strip_lemmaE)
 done