--- a/thys/recursive.thy	Wed Feb 06 04:11:06 2013 +0000
+++ b/thys/recursive.thy	Wed Feb 06 04:27:03 2013 +0000
@@ -4879,10 +4879,18 @@
 apply(drule_tac x="length args" in meta_spec)
 apply(drule_tac x="tm_of (a [+] dummy_abc (length args))" in meta_spec)
 apply(auto)
-apply(rule_tac x="m" in exI)
-apply(rule_tac x="n" in exI)
 apply(simp add: tape_of_nat_abv)
 apply(subgoal_tac "b = length args")
+apply(simp add: Hoare_halt_def)
+apply(auto)[1]
+apply(rule_tac x="na" in exI)
+apply(auto)[1]
+apply(case_tac "steps0 (Suc 0, [Bk, Bk], <args>)
+                                   (tm_of (a [+] dummy_abc (length args)) @
+                                    shift (mopup (length args))
+                                     (listsum
+ (layout_of (a [+] dummy_abc (length args)))))
+                                   na")
 apply(simp)
 by (metis assms para_pattern)