diff -r a2dca9a3d0da -r 15ec9b3c14cc src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Fri May 13 13:45:20 2011 +0200
+++ b/src/HOL/TLA/Action.thy	Fri May 13 14:04:47 2011 +0200
@@ -277,16 +277,20 @@
    The following tactic combines these steps except the final one.
 *)
 
-fun enabled_tac (cs, ss) base_vars =
-  clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss);
+fun enabled_tac ctxt base_vars =
+  clarsimp_tac (claset_of ctxt addSIs [base_vars RS @{thm base_enabled}], simpset_of ctxt);
 *}
 
+method_setup enabled = {*
+  Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
+*} ""
+
 (* Example *)
 
 lemma
   assumes "basevars (x,y,z)"
   shows "|- x --> Enabled ($x & (y$ = #False))"
-  apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *})
+  apply (enabled assms)
   apply auto
   done