diff -r df4c7bb6c79e -r 251e192339b7 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Wed Jan 16 15:17:02 2013 +0000
+++ b/thys/uncomputable.thy	Thu Jan 17 11:51:00 2013 +0000
@@ -1071,13 +1071,6 @@
   and the final configuration is standard.
 *}
 
-
-fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" ("< _ >" [0] 100)
-  where 
-  "tape_of_nat_list [] = []" |
-  "tape_of_nat_list [n] = Oc\<up>(Suc n)" |
-  "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)"
-
 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
   where
   "haltP t lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) t n = (0, Bk\<up>a,  Oc\<up>b @ Bk\<up>c))"
@@ -1341,7 +1334,7 @@
         using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h
         apply(auto)
         apply(rule_tac x = na in exI)
-        apply(simp add: replicate_Suc)
+        apply(simp add: replicate_Suc tape_of_nl_abv)
         done
     qed
   next
@@ -1364,8 +1357,9 @@
     apply(erule_tac x = n in allE)
     apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
     apply(simp, auto)
-    apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
-    apply(simp add: numeral_2_eq_2 replicate_Suc)
+    apply(erule_tac x = nd in allE, erule_tac x = 2 in allE)
+    apply(simp add: numeral_2_eq_2 replicate_Suc tape_of_nl_abv)
+    apply(erule_tac x = 0 in allE, simp)
     done
 qed
   
@@ -1416,7 +1410,7 @@
         using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h
         apply(auto)
         apply(rule_tac x = na in exI)
-        apply(simp add: replicate_Suc)
+        apply(simp add: replicate_Suc tape_of_nl_abv)
         done
     qed
   next
@@ -1434,7 +1428,8 @@
     using h
     apply(auto simp: haltP_def Hoare_unhalt_def)
     apply(erule_tac x = n in allE)
-    apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n", simp)
+    apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
+    apply(simp add: tape_of_nl_abv)
     done
 qed