# HG changeset patch
# User wenzelm
# Date 1364591582 -3600
# Node ID ec3b78ce0758f6db93e0a9c9846a5844afdfc522
# Parent  969ad6538b8fef63f42fef76be08f5bfab6d479a
tuned message;

diff -r 969ad6538b8f -r ec3b78ce0758 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Mar 29 11:32:07 2013 +0100
+++ b/src/HOL/Orderings.thy	Fri Mar 29 22:13:02 2013 +0100
@@ -428,7 +428,7 @@
       [Pretty.str s, Pretty.str ":", Pretty.brk 1,
        Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
   in
-    Pretty.writeln (Pretty.big_list "Order structures:" (map pretty_struct structs))
+    Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
   end;