1.1 --- a/src/HOL/IMP/Compiler.thy	Mon Oct 07 19:01:51 2002 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Tue Oct 08 08:20:17 2002 +0200
     1.3 @@ -97,10 +97,8 @@
     1.4  apply(rule iffI)
     1.5   defer apply simp
     1.6  apply(subgoal_tac "n \<le> size p1")
     1.7 - apply(rotate_tac -1)
     1.8   apply simp
     1.9  apply(rule ccontr)
    1.10 -apply(rotate_tac -1)
    1.11  apply(drule_tac f = length in arg_cong)
    1.12  apply simp
    1.13  apply arith