--- a/src/HOL/Bali/Example.thy Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/Bali/Example.thy Sat Dec 14 17:28:05 2013 +0100
@@ -894,7 +894,7 @@
declare member_is_static_simp [simp]
declare wt.Skip [rule del] wt.Init [rule del]
-ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
+ML {* bind_thms ("wt_intros", map (rewrite_rule @{context} @{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
@@ -1189,7 +1189,7 @@
ML {* bind_thms ("eval_intros", map
(simplify (@{context} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o
- rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
+ rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
axiomatization