src/HOL/Bali/Example.thy

--- a/src/HOL/Bali/Example.thy	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Bali/Example.thy	Thu Apr 18 17:07:01 2013 +0200
@@ -1188,8 +1188,7 @@
         Base_foo_defs  [simp]
 
 ML {* bind_thms ("eval_intros", map 
-        (simplify (@{simpset} delsimps @{thms Skip_eq}
-                             addsimps @{thms lvar_def}) o 
+        (simplify (@{context} 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