--- a/thys/Recursive.thy	Wed Mar 27 09:47:02 2013 +0000
+++ b/thys/Recursive.thy	Wed Mar 27 13:16:37 2013 +0000
@@ -2519,23 +2519,32 @@
 qed
 
 lemma recursive_compile_to_tm_correct2: 
-  assumes  compile: "rec_ci recf = (ap, ary, fp)"
-  and termi: " terminate recf args"
+  assumes termi: " terminate recf args"
   shows "\<exists> stp m l. steps0 (Suc 0, [Bk, Bk], <args>) (tm_of_rec recf) stp = 
                      (0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_exec recf args) @ Bk\<up>l)"
-using recursive_compile_to_tm_correct1[of recf ap ary fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0]
-assms param_pattern[of recf args ap ary fp]
-by(simp add: exp_suc replicate_Suc[THEN sym] del: replicate_Suc tm_of_rec_def)
+proof(case_tac "rec_ci recf", simp add: tm_of_rec.simps)
+  fix ap ar fp
+  assume "rec_ci recf = (ap, ar, fp)"
+  thus "\<exists>stp m l. steps0 (Suc 0, [Bk, Bk], <args>) 
+    (tm_of (ap [+] dummy_abc ar) @ shift (mopup ar) (listsum (layout_of (ap [+] dummy_abc ar)))) stp =
+    (0, Bk # Bk # Bk \<up> m, Oc # Oc \<up> rec_exec recf args @ Bk \<up> l)"
+    using recursive_compile_to_tm_correct1[of recf ap ar fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0]
+      assms param_pattern[of recf args ap ar fp]
+    by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc tm_of_rec_def, 
+      simp add: exp_suc del: replicate_Suc)
+qed
 
 lemma recursive_compile_to_tm_correct3: 
-  assumes compile: "rec_ci recf = (ap, ary, fp)"
-  and termi: "terminate recf args"
-  shows "{\<lambda> (l, r). l = [Bk, Bk] \<and> r = <args>} (tm_of_rec recf) 
-         {\<lambda> (l, r). \<exists> m i. l = Bk\<up>(Suc (Suc m)) \<and> r = Oc\<up>Suc (rec_exec recf args) @ Bk \<up> i}"
-using recursive_compile_to_tm_correct2[of recf ap ary fp args] assms
-apply(simp add: Hoare_halt_def, auto)
-apply(rule_tac x = stp in exI, simp)
-done
+  assumes termi: "terminate recf args"
+  shows "{\<lambda> tp. tp =([Bk, Bk], <args>)} (tm_of_rec recf) 
+         {\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_exec recf args> @ Bk \<up> l)}"
+using recursive_compile_to_tm_correct2[OF assms]
+apply(auto simp add: Hoare_halt_def)
+apply(rule_tac x = stp in exI)
+apply(auto simp add: tape_of_nat_abv)
+apply(rule_tac x = "Suc (Suc m)" in exI)
+apply(simp)
+done 
 
 lemma [simp]:
   "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow>