src/HOL/Bali/Example.thy
changeset 26342 0f65fa163304
parent 24019 67bde7cfcf10
child 26480 544cef16045b
--- 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