diff -r a46362d2b19b -r a013a9dd370f src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/IMP/Compiler.thy	Tue Oct 08 08:20:17 2002 +0200
@@ -97,10 +97,8 @@
 apply(rule iffI)
  defer apply simp
 apply(subgoal_tac "n \<le> size p1")
- apply(rotate_tac -1)
  apply simp
 apply(rule ccontr)
-apply(rotate_tac -1)
 apply(drule_tac f = length in arg_cong)
 apply simp
 apply arith