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