1.1 --- a/src/HOL/TLA/TLA.thy	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -583,11 +583,13 @@
     1.4  
     1.5  ML {*
     1.6  (* inv_tac reduces goals of the form ... ==> sigma |= []P *)
     1.7 -fun inv_tac css = SELECT_GOAL
     1.8 -     (EVERY [auto_tac css,
     1.9 -             TRY (merge_box_tac 1),
    1.10 -             rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
    1.11 -             TRYALL (etac @{thm Stable})]);
    1.12 +fun inv_tac ctxt =
    1.13 +  SELECT_GOAL
    1.14 +    (EVERY
    1.15 +     [auto_tac ctxt,
    1.16 +      TRY (merge_box_tac 1),
    1.17 +      rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
    1.18 +      TRYALL (etac @{thm Stable})]);
    1.19  
    1.20  (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
    1.21     in simple cases it may be able to handle goals like |- MyProg --> []Inv.
    1.22 @@ -595,15 +597,15 @@
    1.23     auto-tactic, which applies too much propositional logic and simplifies
    1.24     too late.
    1.25  *)
    1.26 -fun auto_inv_tac ss = SELECT_GOAL
    1.27 -    ((inv_tac (@{claset}, ss) 1) THEN
    1.28 -     (TRYALL (action_simp_tac
    1.29 -       (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
    1.30 +fun auto_inv_tac ss =
    1.31 +  SELECT_GOAL
    1.32 +    (inv_tac (map_simpset_local (K ss) @{context}) 1 THEN
    1.33 +      (TRYALL (action_simp_tac
    1.34 +        (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
    1.35  *}
    1.36  
    1.37  method_setup invariant = {*
    1.38 -  Method.sections Clasimp.clasimp_modifiers
    1.39 -    >> (K (SIMPLE_METHOD' o inv_tac o clasimpset_of))
    1.40 +  Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
    1.41  *} ""
    1.42  
    1.43  method_setup auto_invariant = {*