1.1 --- a/src/HOL/Orderings.thy	Mon Mar 30 22:43:45 2009 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Mon Mar 30 22:48:15 2009 +0200
     1.3 @@ -384,15 +384,11 @@
     1.4  
     1.5  (** Diagnostic command **)
     1.6  
     1.7 -val print = Toplevel.unknown_context o
     1.8 -  Toplevel.keep (Toplevel.node_case
     1.9 -    (Context.cases (print_structures o ProofContext.init) print_structures)
    1.10 -    (print_structures o Proof.context_of));
    1.11 -
    1.12  val _ =
    1.13    OuterSyntax.improper_command "print_orders"
    1.14      "print order structures available to transitivity reasoner" OuterKeyword.diag
    1.15 -    (Scan.succeed (Toplevel.no_timing o print));
    1.16 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.17 +        Toplevel.keep (print_structures o Toplevel.context_of)));
    1.18  
    1.19  
    1.20  (** Setup **)