--- a/thys/UTM.thy	Wed Feb 06 04:32:18 2013 +0000
+++ b/thys/UTM.thy	Wed Feb 06 04:39:08 2013 +0000
@@ -711,8 +711,8 @@
 by(simp)
 
 lemma tape_of_nl_cons_app1: "(<a # xs @ [b]>) = (Oc\<up>(Suc a) @ Bk # (<xs@ [b]>))"
-apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps)
-apply(simp add: tape_of_nl_abv  tape_of_nat_list.simps)
+apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(simp add: tape_of_nl_abv  tape_of_nat_list.simps tape_of_nat_abv)
 done
 
 lemma bl_bin_bk_oc[simp]:
@@ -1231,7 +1231,7 @@
       done
   qed
   thus "?thesis"
-    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
     done
 qed