--- 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;