src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy

--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri May 13 23:58:40 2011 +0200
@@ -606,7 +606,7 @@
 fun abstraction_tac ctxt =
   SELECT_GOAL (auto_tac
     (ctxt addSIs @{thms weak_strength_lemmas}
-      |> map_simpset_local (fn ss =>
+      |> map_simpset (fn ss =>
         ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])))
 *}