--- 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)