--- a/src/HOL/Tools/split_rule.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/split_rule.ML Wed Dec 16 16:31:36 2015 +0100
@@ -113,10 +113,10 @@
Theory.setup
(Attrib.setup @{binding split_format}
(Scan.lift (Args.parens (Args.$$$ "complete")
- >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
+ >> K (Thm.rule_attribute [] (complete_split_rule o Context.proof_of))))
"split pair-typed subterms in premises, or function arguments" #>
Attrib.setup @{binding split_rule}
- (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
+ (Scan.succeed (Thm.rule_attribute [] (split_rule o Context.proof_of)))
"curries ALL function variables occurring in a rule's conclusion");
end;