--- a/abacus.thy	Sat Jan 12 01:05:01 2013 +0000
+++ b/abacus.thy	Sat Jan 12 01:33:20 2013 +0000
@@ -6318,7 +6318,7 @@
     apply(rule_tac mopup_halt_bef, auto)
     done
   from h1 and h2 and h3 show 
-    "\<exists>stp. case t_steps tc (tm_of aprog @ abacus.tshift (mop_bef n @ abacus.tshift mp_up (2 * n))
+    "\<exists>stp. case t_steps tc (tm_of aprog @ tshift (mop_bef n @ tshift mp_up (2 * n))
     (start_of (layout_of aprog) (length aprog) - Suc 0), 0) stp of (s, ab)
     \<Rightarrow> s = 0 \<and> mopup_inv (0, ab) am n ires"
   proof(erule_tac exE,