src/HOL/Tools/BNF/bnf_def.ML

             Pretty.quote (Syntax.pretty_term ctxt map)]] @
           List.map (pretty_set sets) (0 upto length sets - 1) @
           [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;
 
 val _ =
   Outer_Syntax.command @{command_spec "print_bnfs"}