changeset 60097 | d20ca79d50e4 |
parent 59936 | b8ffc3dc9e24 |
child 60758 | d8d85a8172b5 |
--- a/src/HOL/Orderings.thy Thu Apr 16 15:11:04 2015 +0200 +++ b/src/HOL/Orderings.thy Thu Apr 16 15:22:44 2015 +0200 @@ -441,8 +441,7 @@ val _ = Outer_Syntax.command @{command_keyword print_orders} "print order structures available to transitivity reasoner" - (Scan.succeed (Toplevel.unknown_context o - Toplevel.keep (print_structures o Toplevel.context_of))); + (Scan.succeed (Toplevel.keep (print_structures o Toplevel.context_of))); (* tactics *)