src/HOL/Bali/TypeSafe.thy

                 \<rbrakk> \<Longrightarrow> P L accC (Norm s0) \<langle>If(e) c1 Else c2\<rangle>\<^sub>s \<diamondsuit> s2" 
    shows "P L accC s0 t v s1"  
 proof -
   note inj_term_simps [simp]
   from eval 
-  show "\<And> L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
+  have "\<And>L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
                        \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
         \<Longrightarrow> P L accC s0 t v s1" (is "PROP ?Hyp s0 t v s1")
   proof (induct)
     case Abrupt with abrupt show ?case .
   next