diff -r 6013ca0e6e22 -r eccd79a974ae thys/UTM.thy
--- a/thys/UTM.thy	Wed Feb 13 20:08:14 2013 +0000
+++ b/thys/UTM.thy	Thu Feb 14 09:31:19 2013 +0000
@@ -5086,16 +5086,16 @@
 
 lemma tutm_uhalt': 
 assumes tm_wf:  "tm_wf (tp,0)"
-  and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))"
-  shows "\<forall> stp. \<not> is_final (steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp)"
-apply(simp add: t_utm_def)
+  and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (1, Bk\<up>(l), <lm>) tp stp))"
+  shows "\<forall> stp. \<not> is_final (steps0 (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp)"
+unfolding t_utm_def
 proof(rule_tac compile_correct_unhalt)
   show "layout_of F_aprog = layout_of F_aprog" by simp
 next
   show "F_tprog = tm_of F_aprog"
     by(simp add:  F_tprog_def)
 next
-  show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>)  []"
+  show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>)  []"
     by(auto simp: crsp.simps start_of.simps)
 next
   show "length F_tprog div 2 = length F_tprog div 2" by simp
@@ -5154,7 +5154,7 @@
     \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))\<rbrakk>
   \<Longrightarrow> \<forall> stp. \<not> is_final (steps0 (Suc 0, Bk\<up>(m), <[code tp, bl2wc (<args>)]> @ Bk\<up>(n)) t_utm stp)"
 apply(rule_tac tape_normalize)
-apply(rule_tac tutm_uhalt', simp_all)
+apply(rule_tac tutm_uhalt'[simplified], simp_all)
 done
 
 lemma UTM_uhalt_lemma_pre: