src/HOL/Orderings.thy
changeset 51658 21c10672633b
parent 51579 ec3b78ce0758
child 51717 9e7d1c139569
--- a/src/HOL/Orderings.thy	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/HOL/Orderings.thy	Tue Apr 09 15:29:25 2013 +0200
@@ -492,8 +492,8 @@
 val _ =
   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)));
+    (Scan.succeed (Toplevel.unknown_context o
+      Toplevel.keep (print_structures o Toplevel.context_of)));
 
 end;