diff --git a/src/Pure/General/output.ML b/src/Pure/General/output.ML
--- a/src/Pure/General/output.ML
+++ b/src/Pure/General/output.ML
@@ -1,199 +1,162 @@
 (*  Title:      Pure/General/output.ML
     Author:     Makarius
 
 Isabelle output channels.
 *)
 
 signature BASIC_OUTPUT =
 sig
   val writeln: string -> unit
   val tracing: string -> unit
   val warning: string -> unit
   val legacy_feature: string -> unit
-  val profile_time: ('a -> 'b) -> 'a -> 'b
-  val profile_time_thread: ('a -> 'b) -> 'a -> 'b
-  val profile_allocations: ('a -> 'b) -> 'a -> 'b
 end;
 
 signature OUTPUT =
 sig
   include BASIC_OUTPUT
   type output = string
   val default_output: string -> output * int
   val default_escape: output -> string
   val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
   val output_width: string -> output * int
   val output: string -> output
   val escape: output -> string
   val physical_stdout: output -> unit
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
   type protocol_message_fn = Output_Primitives.protocol_message_fn
   exception Protocol_Message of Properties.T
   val protocol_message_undefined: protocol_message_fn
   val writelns: string list -> unit
   val state: string -> unit
   val information: string -> unit
   val error_message': serial * string -> unit
   val error_message: string -> unit
   val system_message: string -> unit
   val status: string list -> unit
   val report: string list -> unit
   val result: Properties.T -> string list -> unit
   val protocol_message: protocol_message_fn
   val try_protocol_message: protocol_message_fn
 end;
 
 signature PRIVATE_OUTPUT =
 sig
   include OUTPUT
   val writeln_fn: (output list -> unit) Unsynchronized.ref
   val state_fn: (output list -> unit) Unsynchronized.ref
   val information_fn: (output list -> unit) Unsynchronized.ref
   val tracing_fn: (output list -> unit) Unsynchronized.ref
   val warning_fn: (output list -> unit) Unsynchronized.ref
   val legacy_fn: (output list -> unit) Unsynchronized.ref
   val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
   val system_message_fn: (output list -> unit) Unsynchronized.ref
   val status_fn: (output list -> unit) Unsynchronized.ref
   val report_fn: (output list -> unit) Unsynchronized.ref
   val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
   val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref
 end;
 
 structure Private_Output: PRIVATE_OUTPUT =
 struct
 
 (** print modes **)
 
 type output = string;  (*raw system output*)
 
 fun default_output s = (s, size s);
 fun default_escape (s: output) = s;
 
 local
   val default = {output = default_output, escape = default_escape};
   val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
 in
   fun add_mode name output escape =
     if Thread_Data.is_virtual then ()
     else Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
   fun get_mode () =
     the_default default
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
 fun output_width x = #output (get_mode ()) x;
 val output = #1 o output_width;
 
 fun escape x = #escape (get_mode ()) x;
 
 
 
 (** output channels **)
 
 (* primitives -- provided via bootstrap environment *)
 
 val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn;
 val state_fn = Unsynchronized.ref Output_Primitives.state_fn;
 val information_fn = Unsynchronized.ref Output_Primitives.information_fn;
 val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn;
 val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn;
 val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn;
 val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn;
 val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn;
 val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
 val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
 val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
 
 type protocol_message_fn = Output_Primitives.protocol_message_fn;
 val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
 
 
 (* physical output -- not to be used in user-space *)
 
 fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
 fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
 
 fun physical_writeln "" = ()
   | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
 
 
 (* Isabelle output channels *)
 
 exception Protocol_Message of Properties.T;
 
 val protocol_message_undefined: Output_Primitives.protocol_message_fn =
   fn props => fn _ => raise Protocol_Message props;
 
 fun init_channels () =
  (writeln_fn := (physical_writeln o implode);
   state_fn := (fn ss => ! writeln_fn ss);
   information_fn := Output_Primitives.ignore_outputs;
   tracing_fn := (fn ss => ! writeln_fn ss);
   warning_fn := (physical_writeln o prefix_lines "### " o implode);
   legacy_fn := (fn ss => ! warning_fn ss);
   error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
   system_message_fn := (fn ss => ! writeln_fn ss);
   status_fn := Output_Primitives.ignore_outputs;
   report_fn := Output_Primitives.ignore_outputs;
   result_fn := (fn _ => Output_Primitives.ignore_outputs);
   protocol_message_fn := protocol_message_undefined);
 
 val _ = if Thread_Data.is_virtual then () else init_channels ();
 
 fun writelns ss = ! writeln_fn (map output ss);
 fun writeln s = writelns [s];
 fun state s = ! state_fn [output s];
 fun information s = ! information_fn [output s];
 fun tracing s = ! tracing_fn [output s];
 fun warning s = ! warning_fn [output s];
 fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)];
 fun error_message' (i, s) = ! error_message_fn (i, [output s]);
 fun error_message s = error_message' (serial (), s);
 fun system_message s = ! system_message_fn [output s];
 fun status ss = ! status_fn (map output ss);
 fun report ss = ! report_fn (map output ss);
 fun result props ss = ! result_fn props (map output ss);
 fun protocol_message props body = ! protocol_message_fn props body;
 fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
 
-
-(* profiling *)
-
-local
-
-fun output_profile title entries =
-  let
-    val body = entries
-      |> sort (int_ord o apply2 fst)
-      |> map (fn (count, name) =>
-          let
-            val c = string_of_int count;
-            val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
-          in prefix ^ c ^ " " ^ name end);
-    val total = fold (curry (op +) o fst) entries 0;
-  in
-    if total = 0 then ()
-    else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
-  end;
-
-in
-
-fun profile_time f x =
-  ML_Profiling.profile_time (output_profile "time profile:") f x;
-
-fun profile_time_thread f x =
-  ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x;
-
-fun profile_allocations f x =
-  ML_Profiling.profile_allocations (output_profile "allocations profile:") f x;
-
-end;
-
-
 end;
 
 structure Output: OUTPUT = Private_Output;
 structure Basic_Output: BASIC_OUTPUT = Output;
 open Basic_Output;
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,26 +1,44 @@
 (*  Title:      Pure/ML/ml_profiling.ML
     Author:     Makarius
 
 ML profiling.
 *)
 
 signature ML_PROFILING =
 sig
-  val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
-  val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
-  val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
+  val profile_time: ('a -> 'b) -> 'a -> 'b
+  val profile_time_thread: ('a -> 'b) -> 'a -> 'b
+  val profile_allocations: ('a -> 'b) -> 'a -> 'b
 end;
 
 structure ML_Profiling: ML_PROFILING =
 struct
 
-fun profile_time pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+fun profile mode title =
+  mode |> PolyML.Profiling.profileStream (fn entries =>
+    let
+      val body = entries
+        |> sort (int_ord o apply2 fst)
+        |> map (fn (count, name) =>
+            let
+              val c = string_of_int count;
+              val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
+            in prefix ^ c ^ " " ^ name end);
+      val total = fold (curry (op +) o fst) entries 0;
+    in
+      if total = 0 then ()
+      else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
+    end);
 
-fun profile_time_thread pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+fun profile_time f =
+  profile PolyML.Profiling.ProfileTime "time profile:" f;
 
-fun profile_allocations pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+fun profile_time_thread f =
+  profile PolyML.Profiling.ProfileTimeThisThread "time profile (this thread):" f;
+
+fun profile_allocations f =
+  profile PolyML.Profiling.ProfileAllocations "allocations profile:" f;
 
 end;
+
+open ML_Profiling;
diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML
+++ b/src/Pure/ROOT.ML
@@ -1,358 +1,358 @@
 (*  Title:      Pure/ROOT.ML
     Author:     Makarius
 
 Main entry point for the Isabelle/Pure bootstrap process.
 
 Note: When this file is open in the Prover IDE, the ML files of
 Isabelle/Pure can be explored interactively. This is a separate copy of
 Pure within Pure: it does not affect the running logic session.
 *)
 
 chapter "Isabelle/Pure bootstrap";
 
 ML_file "ML/ml_name_space.ML";
 
 
 section "Bootstrap phase 0: Poly/ML setup";
 
 ML_file "ML/ml_init.ML";
 ML_file "ML/ml_system.ML";
 
 ML_file "General/basics.ML";
 ML_file "General/symbol_explode.ML";
 
 ML_file "Concurrent/multithreading.ML";
 ML_file "Concurrent/unsynchronized.ML";
 ML_file "Concurrent/synchronized.ML";
 ML_file "Concurrent/counter.ML";
 
 ML_file "ML/ml_heap.ML";
-ML_file "ML/ml_profiling.ML";
 ML_file "ML/ml_print_depth0.ML";
 ML_file "ML/ml_pretty.ML";
 ML_file "ML/ml_compiler0.ML";
 
 
 section "Bootstrap phase 1: towards ML within position context";
 
 subsection "Library of general tools";
 
 ML_file "library.ML";
 ML_file "General/print_mode.ML";
 ML_file "General/alist.ML";
 ML_file "General/table.ML";
 
 ML_file "General/random.ML";
 ML_file "General/value.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
 ML_file "PIDE/markup.ML";
+ML_file "ML/ml_profiling.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
 ML_file "General/source.ML";
 ML_file "General/symbol.ML";
 ML_file "General/position.ML";
 ML_file "General/symbol_pos.ML";
 ML_file "General/input.ML";
 ML_file "General/comment.ML";
 ML_file "General/antiquote.ML";
 ML_file "ML/ml_lex.ML";
 ML_file "ML/ml_compiler1.ML";
 
 
 section "Bootstrap phase 2: towards ML within Isar context";
 
 subsection "Library of general tools";
 
 ML_file "General/integer.ML";
 ML_file "General/stack.ML";
 ML_file "General/queue.ML";
 ML_file "General/heap.ML";
 ML_file "General/same.ML";
 ML_file "General/ord_list.ML";
 ML_file "General/balanced_tree.ML";
 ML_file "General/linear_set.ML";
 ML_file "General/buffer.ML";
 ML_file "General/pretty.ML";
 ML_file "General/rat.ML";
 ML_file "PIDE/xml.ML";
 ML_file "General/path.ML";
 ML_file "General/url.ML";
 ML_file "System/bash.ML";
 ML_file "General/file.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/socket_io.ML";
 ML_file "General/seq.ML";
 ML_file "General/time.ML";
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";
 
 ML_file "PIDE/yxml.ML";
 ML_file "PIDE/byte_message.ML";
 ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document_id.ML";
 
 ML_file "General/change_table.ML";
 ML_file "General/graph.ML";
 
 ML_file "System/options.ML";
 
 
 subsection "Fundamental structures";
 
 ML_file "name.ML";
 ML_file "term.ML";
 ML_file "context.ML";
 ML_file "config.ML";
 ML_file "context_position.ML";
 ML_file "soft_type_system.ML";
 
 
 subsection "Concurrency within the ML runtime";
 
 ML_file "ML/exn_properties.ML";
 ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
 ML_file "Concurrent/isabelle_thread.ML";
 ML_file "Concurrent/single_assignment.ML";
 
 ML_file "Concurrent/par_exn.ML";
 ML_file "Concurrent/task_queue.ML";
 ML_file "Concurrent/future.ML";
 ML_file "Concurrent/event_timer.ML";
 ML_file "Concurrent/timeout.ML";
 ML_file "Concurrent/lazy.ML";
 ML_file "Concurrent/par_list.ML";
 
 ML_file "Concurrent/mailbox.ML";
 ML_file "Concurrent/cache.ML";
 
 ML_file "PIDE/active.ML";
 ML_file "Thy/export.ML";
 
 
 subsection "Inner syntax";
 
 ML_file "Syntax/type_annotation.ML";
 ML_file "Syntax/term_position.ML";
 ML_file "Syntax/lexicon.ML";
 ML_file "Syntax/ast.ML";
 ML_file "Syntax/syntax_ext.ML";
 ML_file "Syntax/parser.ML";
 ML_file "Syntax/syntax_trans.ML";
 ML_file "Syntax/mixfix.ML";
 ML_file "Syntax/printer.ML";
 ML_file "Syntax/syntax.ML";
 
 
 subsection "Core of tactical proof system";
 
 ML_file "term_ord.ML";
 ML_file "term_subst.ML";
 ML_file "General/completion.ML";
 ML_file "General/name_space.ML";
 ML_file "sorts.ML";
 ML_file "type.ML";
 ML_file "logic.ML";
 ML_file "Syntax/simple_syntax.ML";
 ML_file "net.ML";
 ML_file "item_net.ML";
 ML_file "envir.ML";
 ML_file "consts.ML";
 ML_file "term_xml.ML";
 ML_file "primitive_defs.ML";
 ML_file "sign.ML";
 ML_file "defs.ML";
 ML_file "term_sharing.ML";
 ML_file "pattern.ML";
 ML_file "unify.ML";
 ML_file "theory.ML";
 ML_file "proofterm.ML";
 ML_file "thm.ML";
 ML_file "more_pattern.ML";
 ML_file "more_unify.ML";
 ML_file "more_thm.ML";
 
 ML_file "facts.ML";
 ML_file "thm_name.ML";
 ML_file "global_theory.ML";
 ML_file "pure_thy.ML";
 ML_file "drule.ML";
 ML_file "morphism.ML";
 ML_file "variable.ML";
 ML_file "conv.ML";
 ML_file "goal_display.ML";
 ML_file "tactical.ML";
 ML_file "search.ML";
 ML_file "tactic.ML";
 ML_file "raw_simplifier.ML";
 ML_file "conjunction.ML";
 ML_file "assumption.ML";
 
 
 subsection "Isar -- Intelligible Semi-Automated Reasoning";
 
 (*ML support and global execution*)
 ML_file "ML/ml_syntax.ML";
 ML_file "ML/ml_env.ML";
 ML_file "ML/ml_options.ML";
 ML_file "ML/ml_print_depth.ML";
 ML_file_no_debug "Isar/runtime.ML";
 ML_file "PIDE/execution.ML";
 ML_file "ML/ml_compiler.ML";
 
 ML_file "skip_proof.ML";
 ML_file "goal.ML";
 
 (*outer syntax*)
 ML_file "Isar/keyword.ML";
 ML_file "Isar/token.ML";
 ML_file "Isar/parse.ML";
 ML_file "Thy/document_source.ML";
 ML_file "Thy/thy_header.ML";
 ML_file "Thy/document_marker.ML";
 
 (*proof context*)
 ML_file "Isar/object_logic.ML";
 ML_file "Isar/rule_cases.ML";
 ML_file "Isar/auto_bind.ML";
 ML_file "type_infer.ML";
 ML_file "Syntax/local_syntax.ML";
 ML_file "Isar/proof_context.ML";
 ML_file "type_infer_context.ML";
 ML_file "Syntax/syntax_phases.ML";
 ML_file "Isar/args.ML";
 
 (*theory specifications*)
 ML_file "Isar/local_defs.ML";
 ML_file "Isar/local_theory.ML";
 ML_file "Isar/entity.ML";
 ML_file "PIDE/command_span.ML";
 ML_file "Thy/thy_element.ML";
 ML_file "Thy/markdown.ML";
 ML_file "Thy/latex.ML";
 
 (*ML with context and antiquotations*)
 ML_file "ML/ml_context.ML";
 ML_file "ML/ml_antiquotation.ML";
 ML_file "ML/ml_compiler2.ML";
 ML_file "ML/ml_antiquotations1.ML";
 
 
 section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
 
 (*basic proof engine*)
 ML_file "par_tactical.ML";
 ML_file "context_tactic.ML";
 ML_file "Isar/proof_display.ML";
 ML_file "Isar/attrib.ML";
 ML_file "Isar/context_rules.ML";
 ML_file "Isar/method.ML";
 ML_file "Isar/proof.ML";
 ML_file "Isar/element.ML";
 ML_file "Isar/obtain.ML";
 ML_file "Isar/subgoal.ML";
 ML_file "Isar/calculation.ML";
 
 (*local theories and targets*)
 ML_file "Isar/locale.ML";
 ML_file "Isar/generic_target.ML";
 ML_file "Isar/bundle.ML";
 ML_file "Isar/overloading.ML";
 ML_file "axclass.ML";
 ML_file "Isar/class.ML";
 ML_file "Isar/named_target.ML";
 ML_file "Isar/expression.ML";
 ML_file "Isar/interpretation.ML";
 ML_file "Isar/class_declaration.ML";
 ML_file "Isar/target_context.ML";
 ML_file "Isar/experiment.ML";
 ML_file "simplifier.ML";
 ML_file "Tools/plugin.ML";
 
 (*executable theory content*)
 ML_file "Isar/code.ML";
 
 (*specifications*)
 ML_file "Isar/spec_rules.ML";
 ML_file "Isar/specification.ML";
 ML_file "Isar/parse_spec.ML";
 ML_file "Isar/typedecl.ML";
 
 (*toplevel transactions*)
 ML_file "Isar/proof_node.ML";
 ML_file "Isar/toplevel.ML";
 
 (*proof term operations*)
 ML_file "Proof/proof_rewrite_rules.ML";
 ML_file "Proof/proof_syntax.ML";
 ML_file "Proof/proof_checker.ML";
 ML_file "Proof/extraction.ML";
 
 (*Isabelle system*)
 ML_file "PIDE/protocol_command.ML";
 ML_file "System/scala.ML";
 ML_file "System/process_result.ML";
 ML_file "System/isabelle_system.ML";
 
 
 (*theory documents*)
 ML_file "Thy/term_style.ML";
 ML_file "Isar/outer_syntax.ML";
 ML_file "ML/ml_antiquotations2.ML";
 ML_file "ML/ml_pid.ML";
 ML_file "Thy/document_antiquotation.ML";
 ML_file "Thy/document_output.ML";
 ML_file "Thy/document_antiquotations.ML";
 ML_file "General/graph_display.ML";
 ML_file "pure_syn.ML";
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
 ML_file "PIDE/resources.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "thm_deps.ML";
 ML_file "Thy/export_theory.ML";
 ML_file "Thy/sessions.ML";
 ML_file "PIDE/session.ML";
 ML_file "PIDE/document.ML";
 
 (*theory and proof operations*)
 ML_file "Isar/isar_cmd.ML";
 
 
 subsection "Isabelle/Isar system";
 
 ML_file "System/command_line.ML";
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
 ML_file "System/scala_compiler.ML";
 ML_file "System/isabelle_tool.ML";
 ML_file "Thy/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";
 
 
 subsection "Miscellaneous tools and packages for Pure Isabelle";
 
 ML_file "ML/ml_pp.ML";
 ML_file "ML/ml_thms.ML";
 ML_file "ML/ml_file.ML";
 
 ML_file "Tools/build.ML";
 ML_file "Tools/named_thms.ML";
 ML_file "Tools/print_operation.ML";
 ML_file "Tools/rail.ML";
 ML_file "Tools/rule_insts.ML";
 ML_file "Tools/thy_deps.ML";
 ML_file "Tools/class_deps.ML";
 ML_file "Tools/find_theorems.ML";
 ML_file "Tools/find_consts.ML";
 ML_file "Tools/simplifier_trace.ML";
 ML_file_no_debug "Tools/debugger.ML";
 ML_file "Tools/named_theorems.ML";
 ML_file "Tools/doc.ML";
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML"