diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/Evaln.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -294,7 +294,7 @@
       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
     | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
 
-ML_setup {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
+ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
 declare evaln_AbruptIs [intro!]
 
 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"