src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Orderings.thy	Fri Mar 13 23:50:05 2009 +0100
@@ -397,8 +397,7 @@
 (** Setup **)
 
 val setup =
-  Method.add_methods
-    [("order", Method.ctxt_args (SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
+  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
   Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
 
 end;