src/HOL/Tools/split_rule.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 19735 ff13585fbdab
     1.1 --- a/src/HOL/Tools/split_rule.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/split_rule.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -136,13 +136,13 @@
     1.4  
     1.5  fun split_format x = Attrib.syntax
     1.6    (Scan.lift (Args.parens (Args.$$$ "complete"))
     1.7 -    >> K (Attrib.rule (K complete_split_rule)) ||
     1.8 +    >> K (Thm.rule_attribute (K complete_split_rule)) ||
     1.9    Args.and_list1 (Scan.lift (Scan.repeat Args.name))
    1.10 -    >> (fn xss => Attrib.rule (K (split_rule_goal xss)))) x;
    1.11 +    >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss)))) x;
    1.12  
    1.13  val setup =
    1.14    Attrib.add_attributes
    1.15 -    [("split_format", (split_format, split_format),
    1.16 +    [("split_format", split_format,
    1.17        "split pair-typed subterms in premises, or function arguments")];
    1.18  
    1.19  end;