src/HOL/Orderings.thy
changeset 46961 5c6955f487e5
parent 46950 d0181abdbdac
child 46976 80123a220219
     1.1 --- a/src/HOL/Orderings.thy	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -409,8 +409,8 @@
     1.4  (** Diagnostic command **)
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.improper_command "print_orders"
     1.8 -    "print order structures available to transitivity reasoner" Keyword.diag
     1.9 +  Outer_Syntax.improper_command @{command_spec "print_orders"}
    1.10 +    "print order structures available to transitivity reasoner"
    1.11      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.12          Toplevel.keep (print_structures o Toplevel.context_of)));
    1.13