# HG changeset patch
# User blanchet
# Date 1427446594 -3600
# Node ID f014a2dc0ac878cab8dab59e4156f32be9384ca8
# Parent  fd3a7692e08301b45f97804f48d83dee8d133f65
sort BNFs in output

diff -r fd3a7692e083 -r f014a2dc0ac8 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Mar 27 09:52:57 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Mar 27 09:56:34 2015 +0100
@@ -1609,7 +1609,8 @@
           [Pretty.block [Pretty.str (bdN ^ ":"), Pretty.brk 1,
             Pretty.quote (Syntax.pretty_term ctxt bd)]]);
   in
-    Pretty.big_list "BNFs:" (map pretty_bnf (Symtab.dest (Data.get (Context.Proof ctxt))))
+    Pretty.big_list "Registered bounded natural functors:"
+      (map pretty_bnf (sort_wrt fst (Symtab.dest (Data.get (Context.Proof ctxt)))))
     |> Pretty.writeln
   end;