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