diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/split_rule.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -16,7 +16,7 @@
   include BASIC_SPLIT_RULE
   val split_rule_var: term * thm -> thm
   val split_rule_goal: string list list -> thm -> thm
-  val setup: (theory -> theory) list
+  val setup: theory -> theory
 end;
 
 structure SplitRule: SPLIT_RULE =
@@ -141,9 +141,9 @@
     >> (fn xss => Attrib.rule (K (split_rule_goal xss)))) x;
 
 val setup =
- [Attrib.add_attributes
-  [("split_format", (split_format, split_format),
-    "split pair-typed subterms in premises, or function arguments")]];
+  Attrib.add_attributes
+    [("split_format", (split_format, split_format),
+      "split pair-typed subterms in premises, or function arguments")];
 
 end;