src/HOL/Orderings.thy
changeset 36960 01594f816e3a
parent 36635 080b755377c0
child 37767 a2b7a20d6ea3
--- a/src/HOL/Orderings.thy	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Orderings.thy	Mon May 17 23:54:15 2010 +0200
@@ -422,8 +422,8 @@
 (** Diagnostic command **)
 
 val _ =
-  OuterSyntax.improper_command "print_orders"
-    "print order structures available to transitivity reasoner" OuterKeyword.diag
+  Outer_Syntax.improper_command "print_orders"
+    "print order structures available to transitivity reasoner" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
         Toplevel.keep (print_structures o Toplevel.context_of)));