src/HOL/Bali/Example.thy
changeset 26342 0f65fa163304
parent 24019 67bde7cfcf10
child 26480 544cef16045b
     1.1 --- a/src/HOL/Bali/Example.thy	Wed Mar 19 22:47:39 2008 +0100
     1.2 +++ b/src/HOL/Bali/Example.thy	Wed Mar 19 22:50:42 2008 +0100
     1.3 @@ -1193,7 +1193,7 @@
     1.4          Base_foo_defs  [simp]
     1.5  
     1.6  ML_setup {* bind_thms ("eval_intros", map 
     1.7 -        (simplify (simpset() delsimps @{thms Skip_eq}
     1.8 +        (simplify (@{simpset} delsimps @{thms Skip_eq}
     1.9                               addsimps @{thms lvar_def}) o 
    1.10           rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
    1.11  lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros