--- a/thys/uncomputable.thy	Wed Feb 06 14:14:35 2013 +0000
+++ b/thys/uncomputable.thy	Thu Feb 07 00:46:04 2013 +0000
@@ -996,7 +996,7 @@
 
 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n. tp = (Bk \<up> k,  <n::nat>)))}"
+  "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k,  <n::nat> @ Bk \<up> l)))}"
 
 lemma [intro, simp]: "tm_wf0 tcopy"
 by (auto simp: tcopy_def)
@@ -1108,7 +1108,7 @@
     apply(drule_tac x = n in spec)
     apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
     apply(auto simp add: tape_of_nl_abv)
-    done
+    by (metis append_Nil2 replicate_0)
 qed
 
 (* asumme tcontra halts on its code *)