--- a/Tests/Rec_def2.thy	Thu Mar 07 13:41:05 2013 +0000
+++ b/Tests/Rec_def2.thy	Fri Mar 08 11:10:45 2013 +0000
@@ -15,12 +15,10 @@
   "rec_exec s xs = (Suc (xs ! 0))" |
   "rec_exec (id m n) xs = (xs ! n)" |
   "rec_exec (Cn n f gs) xs = 
-             (let ys = (map (\<lambda> a. rec_exec a xs) gs) in 
-                                  rec_exec f ys)" | 
+     rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" | 
   "rec_exec (Pr n f g) xs = 
-     (if hd xs = 0 then 
-                  rec_exec f (tl xs)
-      else rec_exec g ((hd xs - 1) # tl xs @ [rec_exec (Pr n f g) ((hd xs - 1) # tl xs)]))" |
+     (if hd xs = 0 then rec_exec f (tl xs)
+      else rec_exec g ((hd xs - 1) # (rec_exec (Pr n f g) ((hd xs - 1) # tl xs)) # tl xs))" |
   "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (x # xs) = 0)"
 by pat_completeness auto
 
@@ -29,7 +27,6 @@
 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')
 done
 
-
 inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
   where
   termi_z: "terminate z [n]"
@@ -38,8 +35,7 @@
 | termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); 
               \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs"
 | termi_pr_0: "\<lbrakk>terminate f xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Pr n f g) (0 # xs)"
-| termi_pr_suc: "\<lbrakk>terminate (Pr n f gs) (x # xs);
-                  terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> 
+| termi_pr_suc: "\<lbrakk>terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> 
                   \<Longrightarrow> terminate (Pr n f gs) (Suc x # xs)"
 | termi_mn: "\<lbrakk>length xs = n; rec_exec f (r # xs) = 0;
               \<forall> i < r. terminate f (i # xs) \<and> rec_exec f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"