src/HOL/Bali/AxSem.thy
changeset 27226 5a3e5e46d977
parent 26480 544cef16045b
child 28524 644b62cf678f
     1.1 --- a/src/HOL/Bali/AxSem.thy	Mon Jun 16 17:54:35 2008 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Jun 16 17:54:36 2008 +0200
     1.3 @@ -1013,7 +1013,7 @@
     1.4  apply  (auto simp add: type_ok_def)
     1.5  done
     1.6  
     1.7 -ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
     1.8 +ML {* 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]