--- 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"