diff -r 31cbcb019003 -r bb1d1c6a10bb src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Wed Feb 17 09:08:58 2010 -0800
+++ b/src/HOLCF/ex/Loop.thy	Wed Feb 17 09:22:40 2010 -0800
@@ -115,7 +115,7 @@
   and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
 prefer 2 apply (assumption)
 apply (simp add: step_def2)
-apply (simp del: iterate_Suc add: loop_lemma2)
+apply (drule (1) loop_lemma2, simp)
 done
 
 lemma loop_lemma4 [rule_format]: