diff -r c2b38181b7f1 -r 6f7ac44365d7 src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Wed Mar 16 22:04:38 2016 +0100
+++ b/src/Doc/System/Environment.thy	Wed Mar 16 22:06:05 2016 +0100
@@ -1,4 +1,4 @@
-(*:maxLineLen=78:*)
+     (*:maxLineLen=78:*)
 
 theory Environment
 imports Base
@@ -313,12 +313,8 @@
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
 
   Run the raw Isabelle ML process in batch mode.\<close>}
-\<close>
 
-
-subsubsection \<open>Options\<close>
-
-text \<open>
+  \<^medskip>
   Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
   started. The source is either given literally or taken from a file. Multiple
   \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
@@ -366,17 +362,20 @@
     -m MODE      add print mode for output
     -n           no build of session image on startup
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
-    -r           logic session is RAW_ML_SYSTEM
+    -r           bootstrap from raw Poly/ML
     -s           system build mode for session image
 
   Build a logic session image and run the raw Isabelle ML process
   in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
 
+  \<^medskip>
   Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
-  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
-  abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
-  Isabelle/Pure interactively.
+  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
 
+  Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
+  relevant for Isabelle/Pure development.
+
+  \<^medskip>
   Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
   (\secref{sec:tool-process}).