src/HOL/Tools/split_rule.ML

--- a/src/HOL/Tools/split_rule.ML	Wed Feb 07 18:00:38 2007 +0100
+++ b/src/HOL/Tools/split_rule.ML	Wed Feb 07 18:01:40 2007 +0100
@@ -150,7 +150,9 @@
 val setup =
   Attrib.add_attributes
     [("split_format", split_format,
-      "split pair-typed subterms in premises, or function arguments")];
+      "split pair-typed subterms in premises, or function arguments"),
+     ("split_rule", Attrib.no_args (Thm.rule_attribute (K split_rule)),
+      "curries ALL function variables occurring in a rule's conclusion")];
 
 end;