src/HOL/Bali/Example.thy

 done
 
 
 declare member_is_static_simp [simp]
 declare wt.Skip [rule del] wt.Init [rule del]
-ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
+ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
 lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
 lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
 
 lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
 lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def

 declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
 declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
 declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
         Base_foo_defs  [simp]
 
-ML {* bind_thms ("eval_intros", map 
-        (simplify (simpset() delsimps [thm "Skip_eq"]
-                             addsimps [thm "lvar_def"]) o 
-         rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
+ML_setup {* bind_thms ("eval_intros", map 
+        (simplify (simpset() delsimps @{thms Skip_eq}
+                             addsimps @{thms lvar_def}) o 
+         rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
 
 consts
   a :: loc
   b :: loc