# HG changeset patch
# User wenzelm
# Date 1238446095 -7200
# Node ID 342c7334523740d209318fe4795a262c68b35b21
# Parent  6d321d31914185efb3b16ef59f951a03661c2fa2
simplified 'print_orders' command;

diff -r 6d321d319141 -r 342c73345237 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Mar 30 22:43:45 2009 +0200
+++ b/src/HOL/Orderings.thy	Mon Mar 30 22:48:15 2009 +0200
@@ -384,15 +384,11 @@
 
 (** Diagnostic command **)
 
-val print = Toplevel.unknown_context o
-  Toplevel.keep (Toplevel.node_case
-    (Context.cases (print_structures o ProofContext.init) print_structures)
-    (print_structures o Proof.context_of));
-
 val _ =
   OuterSyntax.improper_command "print_orders"
     "print order structures available to transitivity reasoner" OuterKeyword.diag
-    (Scan.succeed (Toplevel.no_timing o print));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+        Toplevel.keep (print_structures o Toplevel.context_of)));
 
 
 (** Setup **)