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