src/HOL/Orderings.thy
changeset 30515 bca05b17b618
parent 30510 4120fc59dd85
child 30528 7173bf123335
     1.1 --- a/src/HOL/Orderings.thy	Fri Mar 13 23:32:40 2009 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Fri Mar 13 23:50:05 2009 +0100
     1.3 @@ -397,8 +397,7 @@
     1.4  (** Setup **)
     1.5  
     1.6  val setup =
     1.7 -  Method.add_methods
     1.8 -    [("order", Method.ctxt_args (SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
     1.9 +  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
    1.10    Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
    1.11  
    1.12  end;