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; \ -attribute_setup uncurry = \Scan.succeed (Thm.rule_attribute (K uncurry_rule))\ -attribute_setup curry = \Scan.succeed (Thm.rule_attribute (K curry_rule))\ +attribute_setup uncurry = \Scan.succeed (Thm.rule_attribute [] (K uncurry_rule))\ +attribute_setup curry = \Scan.succeed (Thm.rule_attribute [] (K curry_rule))\ end