# HG changeset patch
# User wenzelm
# Date 1305381808 -7200
# Node ID 7ed59879b1b67763c1dbc2da4836c4f24776bf69
# Parent  51d7e74f6899c0b5fbe6df12903ba11ff917e561
proper runtime context for auto_inv_tac;

diff -r 51d7e74f6899 -r 7ed59879b1b6 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Sat May 14 13:32:33 2011 +0200
+++ b/src/HOL/TLA/TLA.thy	Sat May 14 16:03:28 2011 +0200
@@ -597,11 +597,11 @@
    auto-tactic, which applies too much propositional logic and simplifies
    too late.
 *)
-fun auto_inv_tac ss =
+fun auto_inv_tac ctxt =
   SELECT_GOAL
-    (inv_tac (map_simpset (K ss) @{context}) 1 THEN
+    (inv_tac ctxt 1 THEN
       (TRYALL (action_simp_tac
-        (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
+        (simpset_of ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
 *}
 
 method_setup invariant = {*
@@ -609,8 +609,7 @@
 *} ""
 
 method_setup auto_invariant = {*
-  Method.sections Clasimp.clasimp_modifiers
-    >> (K (SIMPLE_METHOD' o auto_inv_tac o simpset_of))
+  Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
 *} ""
 
 lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"