src/HOL/Bali/Evaln.thy
changeset 56199 8e8d28ed7529
parent 54863 82acc20ded73
child 58251 b13e5c3497f5
     1.1 --- a/src/HOL/Bali/Evaln.thy	Tue Mar 18 10:00:23 2014 +0100
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Tue Mar 18 11:07:47 2014 +0100
     1.3 @@ -292,7 +292,7 @@
     1.4        (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
     1.5      | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
     1.6  
     1.7 -ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
     1.8 +ML {* ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
     1.9  declare evaln_AbruptIs [intro!]
    1.10  
    1.11  lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"