--- a/src/HOL/Bali/Evaln.thy Mon Jun 16 17:54:35 2008 +0200
+++ b/src/HOL/Bali/Evaln.thy Mon Jun 16 17:54:36 2008 +0200
@@ -294,7 +294,7 @@
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
| _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
-ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
+ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
declare evaln_AbruptIs [intro!]
lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"