| changeset 27226 | 5a3e5e46d977 |
| parent 26480 | 544cef16045b |
| child 28524 | 644b62cf678f |
--- a/src/HOL/Bali/Eval.thy Mon Jun 16 17:54:35 2008 +0200 +++ b/src/HOL/Bali/Eval.thy Mon Jun 16 17:54:36 2008 +0200 @@ -891,7 +891,7 @@ | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *} ML {* -bind_thms ("AbruptIs", sum3_instantiate @{thm eval.Abrupt}) +bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt}) *} declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!]