src/HOL/Bali/Evaln.thy
changeset 27226 5a3e5e46d977
parent 26932 c398a3866082
child 28524 644b62cf678f
     1.1 --- a/src/HOL/Bali/Evaln.thy	Mon Jun 16 17:54:35 2008 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Jun 16 17:54:36 2008 +0200
     1.3 @@ -294,7 +294,7 @@
     1.4        (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
     1.5      | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
     1.6  
     1.7 -ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
     1.8 +ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
     1.9  declare evaln_AbruptIs [intro!]
    1.10  
    1.11  lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"