diff -r dfe852aacae6 -r 06db15939b7c thys/UF.thy
--- a/thys/UF.thy	Wed Jan 30 03:46:22 2013 +0000
+++ b/thys/UF.thy	Wed Jan 30 09:33:06 2013 +0000
@@ -4473,9 +4473,9 @@
 lemma tape_of_nat_list_butlast_last:
   "ys \<noteq> [] \<Longrightarrow> <ys @ [y]> = <ys> @ Bk # Oc\<up>Suc y"
 apply(induct ys, simp, simp)
-apply(case_tac "ys = []", simp add: tape_of_nl_abv 
+apply(case_tac "ys = []", simp add: tape_of_nl_abv tape_of_nat_abv
                                     tape_of_nat_list.simps)
-apply(simp add: tape_of_nl_cons)
+apply(simp add: tape_of_nl_cons tape_of_nat_abv)
 done
 
 lemma listsum2_append:
@@ -4518,7 +4518,7 @@
     Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)"
     apply(case_tac "xs = []")
     apply(simp add: tape_of_nl_abv listsum2.simps 
-      tape_of_nat_list.simps)
+      tape_of_nat_list.simps tape_of_nat_abv)
     apply(simp add: tape_of_nat_list_butlast_last)
     using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"]
     apply(simp)