# 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 **)