| changeset 27226 | 5a3e5e46d977 |
| parent 26480 | 544cef16045b |
| child 28524 | 644b62cf678f |
--- a/src/HOL/Bali/AxSem.thy Mon Jun 16 17:54:35 2008 +0200 +++ b/src/HOL/Bali/AxSem.thy Mon Jun 16 17:54:36 2008 +0200 @@ -1013,7 +1013,7 @@ apply (auto simp add: type_ok_def) done -ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *} +ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *} declare ax_Abrupts [intro!] lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]