1.1 --- a/src/HOL/IMP/Compiler.thy	Wed Nov 13 19:12:15 2013 +0100
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Nov 14 10:59:22 2013 +0100
     1.3 @@ -138,11 +138,12 @@
     1.4  by (drule exec_appendL[where P'="[instr]"]) simp
     1.5  
     1.6  lemma exec_appendL_if[intro]:
     1.7 -  fixes i i' :: int
     1.8 +  fixes i i' j :: int
     1.9    shows
    1.10    "size P' <= i
    1.11 -   \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk')
    1.12 -   \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')"
    1.13 +   \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (j,s',stk')
    1.14 +   \<Longrightarrow> i' = size P' + j
    1.15 +   \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
    1.16  by (drule exec_appendL[where P'=P']) simp
    1.17  
    1.18  text{* Split the execution of a compound program up into the excution of its