
diff -r d273c24b5776 -r fb7756087101 src/HOL/Eisbach/Eisbach_Tools.thy
--- 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




