--- a/src/HOL/TLA/Action.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/TLA/Action.thy Wed Dec 16 16:31:36 2015 +0100
@@ -123,11 +123,11 @@
\<close>
attribute_setup action_unlift =
- \<open>Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (action_unlift o Context.proof_of))\<close>
attribute_setup action_rewrite =
- \<open>Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (action_rewrite o Context.proof_of))\<close>
attribute_setup action_use =
- \<open>Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (action_use o Context.proof_of))\<close>
(* =========================== square / angle brackets =========================== *)