src/HOL/Tools/split_rule.ML
changeset 11045 971a50fda146
parent 11040 194406da4e43
child 11838 02d75712061d
     1.1 --- a/src/HOL/Tools/split_rule.ML	Sat Feb 03 15:21:57 2001 +0100
     1.2 +++ b/src/HOL/Tools/split_rule.ML	Sat Feb 03 15:22:57 2001 +0100
     1.3 @@ -128,9 +128,10 @@
     1.4  (* attribute syntax *)
     1.5  
     1.6  fun split_format x = Attrib.syntax
     1.7 -  (Args.mode "complete" >> K (Drule.rule_attribute (K complete_split_rule)) ||
     1.8 -    Args.and_list1 (Scan.lift (Scan.repeat Args.name))
     1.9 -      >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
    1.10 +  (Scan.lift (Args.parens (Args.$$$ "complete"))
    1.11 +    >> K (Drule.rule_attribute (K complete_split_rule)) ||
    1.12 +  Args.and_list1 (Scan.lift (Scan.repeat Args.name))
    1.13 +    >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
    1.14  
    1.15  val setup =
    1.16   [Attrib.add_attributes