--- a/thys/Recursive.thy	Wed Feb 27 01:32:53 2013 +0000
+++ b/thys/Recursive.thy	Thu Feb 28 12:37:33 2013 +0000
@@ -92,18 +92,17 @@
   used by @{text "ap"} for its execution. 
 *}
 
-function rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat"
+fun rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat"
   where
   "rec_ci z = (rec_ci_z, 1, 2)" |
   "rec_ci s = (rec_ci_s, 1, 3)" |
   "rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" |
   "rec_ci (Cn n f gs) = 
-      (let cied_gs = map (\<lambda> g. rec_ci g) (f # gs) in
-       let (fprog, fpara, fn) = hd cied_gs in 
-       let pstr = 
-        Max (set (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs))) in
+      (let cied_gs = map (\<lambda> g. rec_ci g) gs in
+       let (fprog, fpara, fn) = rec_ci f in 
+       let pstr = Max (set (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs))) in
        let qstr = pstr + Suc (length gs) in 
-       (cn_merge_gs (tl cied_gs) pstr [+] mv_boxes 0 qstr n [+] 
+       (cn_merge_gs cied_gs pstr [+] mv_boxes 0 qstr n [+] 
           mv_boxes pstr 0 (length gs) [+] fprog [+] 
             mv_box fpara pstr [+] empty_boxes (length gs) [+] 
              mv_box pstr n [+] mv_boxes qstr 0 n, n,  qstr + n))" |
@@ -122,25 +121,6 @@
           let len = length (fprog) in 
             (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
              Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))"
-  by pat_completeness auto
-termination 
-proof
-  show "wf (measure size)" by auto
-next
-  fix n f gs x
-  assume "(x::recf) \<in> set (f # gs)" 
-  thus "(x, Cn n f gs) \<in> measure size"
-    by(induct gs, auto)
-next
-  fix n f g
-  show "(f, Pr n f g) \<in> measure size" by auto
-next
-  fix n f g x xa y xb ya
-  show "(g, Pr n f g) \<in> measure size" by auto
-next
-  fix n f
-  show "(f, Mn n f) \<in> measure size" by auto
-qed
 
 declare rec_ci.simps [simp del] rec_ci_s_def[simp del] 
         rec_ci_z_def[simp del] rec_ci_id.simps[simp del]
@@ -323,8 +303,8 @@
 apply(induct f arbitrary: l x y rule: rec_ci.induct)
 apply(simp add: rec_calc_inj_case_z)
 apply(simp add: rec_calc_inj_case_s)
-apply(simp add: rec_calc_inj_case_id, simp)
-apply(erule rec_calc_inj_case_cn,simp, simp)
+apply(simp add: rec_calc_inj_case_id)
+apply (metis rec_calc_inj_case_cn)
 apply(erule rec_calc_inj_case_pr, auto)
 apply(erule rec_calc_inj_case_mn, auto)
 done