src/HOL/Bali/Eval.thy

  7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
  29(AVar),24(Call)]
 *)
 
 ML {*
-bind_thm ("eval_induct", rearrange_prems 
+ML_Thms.bind_thm ("eval_induct", rearrange_prems 
 [0,1,2,8,4,30,31,27,15,16,
  17,18,19,20,21,3,5,25,26,23,6,
  7,11,9,13,14,12,22,10,28,
  29,24] @{thm eval.induct})
 *}

     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
     | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *}
 
 ML {*
-bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt})
+ML_Thms.bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt})
 *}
 
 declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!]
 
 text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only