src/HOL/Tools/split_rule.ML

 signature SPLIT_RULE =
 sig
   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 =
 struct
 

     >> K (Attrib.rule (K complete_split_rule)) ||
   Args.and_list1 (Scan.lift (Scan.repeat Args.name))
     >> (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;
 
 structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
 open BasicSplitRule;