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

 
 ML {*
 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}])))
 *}
 
 method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""