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;