| changeset 56199 | 8e8d28ed7529 |
| parent 51798 | ad3a241def73 |
| child 58249 | 180f1b3508ed |
--- a/src/HOL/Bali/AxSem.thy Tue Mar 18 10:00:23 2014 +0100 +++ b/src/HOL/Bali/AxSem.thy Tue Mar 18 11:07:47 2014 +0100 @@ -1006,7 +1006,7 @@ apply (auto simp add: type_ok_def) done -ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *} +ML {* ML_Thms.bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *} declare ax_Abrupts [intro!] lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]