--- a/thys/uncomputable.thy	Sat Jan 19 14:44:07 2013 +0000
+++ b/thys/uncomputable.thy	Sat Jan 19 15:27:21 2013 +0000
@@ -984,7 +984,7 @@
 by(auto simp: tm_wf.simps tcopy_end_def)
 
 lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
-apply(auto simp: tm_wf.simps shift.simps adjust.simps length_comp
+apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length
                  tm_comp.simps)
 done