1.1 --- a/src/HOL/TLA/TLA.thy	Fri May 13 23:24:06 2011 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Fri May 13 23:58:40 2011 +0200
     1.3 @@ -599,7 +599,7 @@
     1.4  *)
     1.5  fun auto_inv_tac ss =
     1.6    SELECT_GOAL
     1.7 -    (inv_tac (map_simpset_local (K ss) @{context}) 1 THEN
     1.8 +    (inv_tac (map_simpset (K ss) @{context}) 1 THEN
     1.9        (TRYALL (action_simp_tac
    1.10          (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
    1.11  *}