src/HOL/Eisbach/Eisbach_Tools.thy
changeset 61853 fb7756087101
parent 61818 6de8e7ad95c3
child 63527 59eff6e56d81
--- a/src/HOL/Eisbach/Eisbach_Tools.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -76,7 +76,7 @@
       in Conjunction.curry_balanced (length conjs) thm end;
 \<close>
 
-attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute (K uncurry_rule))\<close>
-attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute (K curry_rule))\<close>
+attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute [] (K uncurry_rule))\<close>
+attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute [] (K curry_rule))\<close>
 
 end