# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1362742264 0
# Node ID 262fc2c6371bd4bbfc6f8643f29f3337964faf84
# Parent  a3ea0b0f8badcd32f2520a6c38e9a9ab33cc83f9
updated

diff -r a3ea0b0f8bad -r 262fc2c6371b Tests/Rec_def2.thy
--- a/Tests/Rec_def2.thy	Fri Mar 08 11:10:45 2013 +0000
+++ b/Tests/Rec_def2.thy	Fri Mar 08 11:31:04 2013 +0000
@@ -35,7 +35,8 @@
 | 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 g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> 
+| termi_pr_suc: "\<lbrakk>terminate (Pr n f gs) (x # xs); length xs = n;
+                  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"