--- a/thys/Recursive.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/thys/Recursive.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -2786,9 +2786,13 @@
 lemma wf_tm_from_abacus: 
   "tp = tm_of ap \<Longrightarrow> 
     tm_wf (tp @ shift( mopup n) (length tp div 2), 0)"
-  using length_start_of_tm[of ap] all_le_start_of[of ap]
+ using length_start_of_tm[of ap] all_le_start_of[of ap]
 apply(auto simp: tm_wf.simps List.list_all_iff)
-done
+apply(case_tac n)
+apply(simp add: mopup.simps)
+apply(simp add: mopup.simps)
+apply (metis mod_mult_right_eq mod_mult_self2 mod_mult_self2_is_0 mult_2_right nat_mult_commute numeral_Bit0)
+sorry
 
 lemma wf_tm_from_recf:
   assumes compile: "tp = tm_of_rec recf"