diff -r c4d16f35c6e7 -r b00508facb4f src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Oct 18 17:41:56 2016 +0200
+++ b/src/Doc/System/Sessions.thy	Wed Oct 19 14:42:28 2016 +0200
@@ -215,6 +215,11 @@
     Isabelle/Scala. Thus it is relatively reliable in canceling processes that
     get out of control, even if there is a deadlock without CPU time usage.
 
+    \<^item> @{system_option_def "profiling"} specifies a mode for global ML
+    profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
+    @{ML profile_time} and \<^verbatim>\<open>allocations\<close> for @{ML profile_allocations}.
+    Results appear near the bottom of the session log file.
+
   The @{tool_def options} tool prints Isabelle system options. Its
   command-line usage is:
   @{verbatim [display]