diff --git a/src/Pure/ML/ml_profiling.ML b/src/Pure/ML/ml_profiling.ML
--- a/src/Pure/ML/ml_profiling.ML
+++ b/src/Pure/ML/ml_profiling.ML
@@ -1,76 +1,76 @@
 (*  Title:      Pure/ML/ml_profiling.ML
     Author:     Makarius
 
 ML profiling (via Poly/ML run-time system).
 *)
 
 signature BASIC_ML_PROFILING =
 sig
   val profile_time: ('a -> 'b) -> 'a -> 'b
   val profile_time_thread: ('a -> 'b) -> 'a -> 'b
   val profile_allocations: ('a -> 'b) -> 'a -> 'b
 end;
 
 signature ML_PROFILING =
 sig
   val check_mode: string -> unit
   val profile: string -> ('a -> 'b) -> 'a -> 'b
   include BASIC_ML_PROFILING
 end;
 
 structure ML_Profiling: ML_PROFILING =
 struct
 
 (* mode *)
 
 val modes =
   Symtab.make
     [("time", PolyML.Profiling.ProfileTime),
      ("time_thread", PolyML.Profiling.ProfileTimeThisThread),
      ("allocations", PolyML.Profiling.ProfileAllocations)];
 
 fun get_mode kind =
   (case Symtab.lookup modes kind of
     SOME mode => mode
   | NONE => error ("Bad profiling mode: " ^ quote kind));
 
 fun check_mode "" = ()
   | check_mode kind = ignore (get_mode kind);
 
 
 (* profile *)
 
 fun print_entry count name =
   let
     val c = string_of_int count;
-    val prefix = Symbol.spaces (Int.max (0, 10 - size c));
+    val prefix = Symbol.spaces (Int.max (0, 12 - size c));
   in prefix ^ c ^ " " ^ name end;
 
 fun profile "" f x = f x
   | profile kind f x =
       let
         val mode = get_mode kind;
         fun output entries =
           (case fold (curry (op +) o fst) entries 0 of
             0 => ()
           | total =>
               let
                 val body = entries
                   |> sort (int_ord o apply2 fst)
                   |> map (fn (count, name) =>
                       let val markup = Markup.ML_profiling_entry {name = name, count = count}
                       in XML.Elem (markup, [XML.Text (print_entry count name ^ "\n")]) end);
                 val head = XML.Text ("profile_" ^ kind ^ ":\n");
                 val foot = XML.Text (print_entry total "TOTAL");
                 val msg = XML.Elem (Markup.ML_profiling kind, head :: body @ [foot]);
               in tracing (YXML.string_of msg) end);
       in PolyML.Profiling.profileStream output mode f x end;
 
 fun profile_time f = profile "time" f;
 fun profile_time_thread f = profile "time_thread" f;
 fun profile_allocations f = profile "allocations" f;
 
 end;
 
 structure Basic_ML_Profiling: BASIC_ML_PROFILING = ML_Profiling;
 open Basic_ML_Profiling;
diff --git a/src/Pure/ML/ml_profiling.scala b/src/Pure/ML/ml_profiling.scala
--- a/src/Pure/ML/ml_profiling.scala
+++ b/src/Pure/ML/ml_profiling.scala
@@ -1,49 +1,49 @@
 /*  Title:      Pure/ML/ml_profiling.scala
     Author:     Makarius
 
 ML profiling (via Poly/ML run-time system).
 */
 
 package isabelle
 
 
 import java.util.Locale
 
 import scala.collection.immutable.SortedMap
 
 
 object ML_Profiling
 {
   sealed case class Entry(name: String, count: Long)
   {
     def clean_name: Entry = copy(name = """-?\(\d+\).*$""".r.replaceAllIn(name, ""))
 
     def print: String =
-      String.format(Locale.ROOT, "%10d %s",
+      String.format(Locale.ROOT, "%12d %s",
         count.asInstanceOf[AnyRef], name.asInstanceOf[AnyRef])
   }
 
   sealed case class Report(kind: String, entries: List[Entry])
   {
     def clean_name: Report = copy(entries = entries.map(_.clean_name))
 
     def total: Entry = Entry("TOTAL", entries.iterator.map(_.count).sum)
 
     def print: String =
       ("profile_" + kind + ":\n") + cat_lines((entries ::: List(total)).map(_.print))
   }
 
   def account(reports: List[Report]): List[Report] =
   {
     val empty = SortedMap.empty[String, Long].withDefaultValue(0L)
     var results = SortedMap.empty[String, SortedMap[String, Long]].withDefaultValue(empty)
     for (report <- reports) {
       val kind = report.kind
       val map = report.entries.foldLeft(results(kind))(
         (m, e) => m + (e.name -> (e.count + m(e.name))))
       results = results + (kind -> map)
     }
     for ((kind, map) <- results.toList)
       yield Report(kind, for ((name, count) <- map.toList.sortBy(_._2)) yield Entry(name, count))
   }
 }