src/HOL/Bali/AxSem.thy
changeset 26480 544cef16045b
parent 26342 0f65fa163304
child 27226 5a3e5e46d977
     1.1 --- a/src/HOL/Bali/AxSem.thy	Sat Mar 29 19:13:58 2008 +0100
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Sat Mar 29 19:14:00 2008 +0100
     1.3 @@ -1013,7 +1013,7 @@
     1.4  apply  (auto simp add: type_ok_def)
     1.5  done
     1.6  
     1.7 -ML_setup {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
     1.8 +ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
     1.9  declare ax_Abrupts [intro!]
    1.10  
    1.11  lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]