diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Wed Mar 19 22:47:39 2008 +0100 +++ b/src/HOL/Bali/Example.thy Wed Mar 19 22:50:42 2008 +0100 @@ -1193,7 +1193,7 @@ Base_foo_defs [simp] ML_setup {* bind_thms ("eval_intros", map - (simplify (simpset() delsimps @{thms Skip_eq} + (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