1.1 --- a/src/HOLCF/ex/Loop.thy	Wed Feb 17 09:08:58 2010 -0800
     1.2 +++ b/src/HOLCF/ex/Loop.thy	Wed Feb 17 09:22:40 2010 -0800
     1.3 @@ -115,7 +115,7 @@
     1.4    and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
     1.5  prefer 2 apply (assumption)
     1.6  apply (simp add: step_def2)
     1.7 -apply (simp del: iterate_Suc add: loop_lemma2)
     1.8 +apply (drule (1) loop_lemma2, simp)
     1.9  done
    1.10  
    1.11  lemma loop_lemma4 [rule_format]: