--- a/thys/abacus.thy	Sun Jan 20 16:01:16 2013 +0000
+++ b/thys/abacus.thy	Tue Jan 22 14:38:56 2013 +0000
@@ -4950,7 +4950,7 @@
     by(case_tac "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp", auto)
 
   then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)"
-    by(auto intro: is_final_steps)
+    by(auto intro: after_is_final)
   then have "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa)"
     using e
     by(simp add: steps_add f)