# HG changeset patch
# User berghofe
# Date 1170867700 -3600
# Node ID 70a7cd02fec148e6a5be1c0a70e436cd0b49ccd5
# Parent  b89dc456dbc6522d6d661fe1d9cfab5f95c75cd9
Added split_rule attribute.

diff -r b89dc456dbc6 -r 70a7cd02fec1 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;