src/HOL/TLA/Action.thy
changeset 61853 fb7756087101
parent 60592 c9bd1d902f04
child 62146 324bc1ffba12
     1.1 --- a/src/HOL/TLA/Action.thy	Tue Dec 15 16:57:10 2015 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Wed Dec 16 16:31:36 2015 +0100
     1.3 @@ -123,11 +123,11 @@
     1.4  \<close>
     1.5  
     1.6  attribute_setup action_unlift =
     1.7 -  \<open>Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of))\<close>
     1.8 +  \<open>Scan.succeed (Thm.rule_attribute [] (action_unlift o Context.proof_of))\<close>
     1.9  attribute_setup action_rewrite =
    1.10 -  \<open>Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of))\<close>
    1.11 +  \<open>Scan.succeed (Thm.rule_attribute [] (action_rewrite o Context.proof_of))\<close>
    1.12  attribute_setup action_use =
    1.13 -  \<open>Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of))\<close>
    1.14 +  \<open>Scan.succeed (Thm.rule_attribute [] (action_use o Context.proof_of))\<close>
    1.15  
    1.16  
    1.17  (* =========================== square / angle brackets =========================== *)