src/HOL/Tools/split_rule.ML
changeset 18708 4b3dadb4fe33
parent 18629 bdf01da93ed4
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/split_rule.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    include BASIC_SPLIT_RULE
     1.5    val split_rule_var: term * thm -> thm
     1.6    val split_rule_goal: string list list -> thm -> thm
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  structure SplitRule: SPLIT_RULE =
    1.12 @@ -141,9 +141,9 @@
    1.13      >> (fn xss => Attrib.rule (K (split_rule_goal xss)))) x;
    1.14  
    1.15  val setup =
    1.16 - [Attrib.add_attributes
    1.17 -  [("split_format", (split_format, split_format),
    1.18 -    "split pair-typed subterms in premises, or function arguments")]];
    1.19 +  Attrib.add_attributes
    1.20 +    [("split_format", (split_format, split_format),
    1.21 +      "split pair-typed subterms in premises, or function arguments")];
    1.22  
    1.23  end;
    1.24