src/HOL/Orderings.thy
changeset 30528 7173bf123335
parent 30515 bca05b17b618
child 30722 623d4831c8cf
     1.1 --- a/src/HOL/Orderings.thy	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Sun Mar 15 15:59:44 2009 +0100
     1.3 @@ -372,13 +372,13 @@
     1.4    Thm.declaration_attribute
     1.5      (fn _ => Data.map (AList.delete struct_eq s));
     1.6  
     1.7 -val attribute = Attrib.syntax
     1.8 -     (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
     1.9 -          Args.del >> K NONE) --| Args.colon (* FIXME ||
    1.10 -        Scan.succeed true *) ) -- Scan.lift Args.name --
    1.11 -      Scan.repeat Args.term
    1.12 -      >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
    1.13 -           | ((NONE, n), ts) => del_struct (n, ts)));
    1.14 +val attribute =
    1.15 +  Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
    1.16 +      Args.del >> K NONE) --| Args.colon (* FIXME ||
    1.17 +    Scan.succeed true *) ) -- Scan.lift Args.name --
    1.18 +  Scan.repeat Args.term
    1.19 +  >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
    1.20 +       | ((NONE, n), ts) => del_struct (n, ts));
    1.21  
    1.22  
    1.23  (** Diagnostic command **)
    1.24 @@ -398,7 +398,7 @@
    1.25  
    1.26  val setup =
    1.27    Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
    1.28 -  Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
    1.29 +  Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
    1.30  
    1.31  end;
    1.32