--- a/src/HOL/Tools/split_rule.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/split_rule.ML Sat Jan 21 23:02:14 2006 +0100
@@ -136,13 +136,13 @@
fun split_format x = Attrib.syntax
(Scan.lift (Args.parens (Args.$$$ "complete"))
- >> K (Attrib.rule (K complete_split_rule)) ||
+ >> K (Thm.rule_attribute (K complete_split_rule)) ||
Args.and_list1 (Scan.lift (Scan.repeat Args.name))
- >> (fn xss => Attrib.rule (K (split_rule_goal xss)))) x;
+ >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss)))) x;
val setup =
Attrib.add_attributes
- [("split_format", (split_format, split_format),
+ [("split_format", split_format,
"split pair-typed subterms in premises, or function arguments")];
end;