diff -r b2f2770ef8d9 -r d1bbea22217b doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Mon Apr 12 16:20:04 1999 +0200
+++ b/doc-src/System/basics.tex	Tue Apr 13 10:34:30 1999 +0200
@@ -113,10 +113,10 @@
 \item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to
   the absolute path names of the \texttt{isabelle} and
   \texttt{isatool} executables, respectively.
-
-\item \settdx{ISABELLE_PATH} and \settdx{ISABELLE_OUTPUT} will have
-  the {\ML} system identifier (as specified by \texttt{ML_SYSTEM})
-  automatically appended to their values.
+  
+\item \settdx{ISABELLE_PATH} and \settdx{ISABELLE_OUTPUT} will have the {\ML}
+  system identifier (according to \texttt{ML_IDENTIFIER} automatically
+  appended to their values.
 \end{itemize}
 
 \medskip The Isabelle settings scheme is basically quite simple, but
@@ -153,18 +153,19 @@
   search path of the shell.
   
 \item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS},
-  \settdx{ML_PLATFORM}] specify the underlying {\ML} system to be used for
-  Isabelle.  The choice of \texttt{ML_SYSTEM} identifiers is quite fixed, see
-  the global \texttt{etc/settings} file for some examples. The actual compiler
-  binary will be run from directory \texttt{ML_HOME}, with \texttt{ML_OPTIONS}
-  as first arguments on the command line.  The optional \texttt{ML_PLATFORM}
-  specifies the binary format of ML heap images, which is useful for
-  cross-platform installations.
-
-\item[\settdx{ISABELLE_PATH}*] is a list of directories (separated by
-  colons) where Isabelle logic images may reside. Note that the
-  \texttt{ML_SYSTEM} identifier is appended to each component
-  automatically.
+  \settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML}
+  system to be used for Isabelle.  The choice of \texttt{ML_SYSTEM}
+  identifiers is quite fixed, see the global \texttt{etc/settings} file for
+  some examples. The actual compiler binary will be run from directory
+  \texttt{ML_HOME}, with \texttt{ML_OPTIONS} as first arguments on the command
+  line.  The optional \texttt{ML_PLATFORM} specifies the binary format of ML
+  heap images, which is useful for cross-platform installations.  The value of
+  \texttt{ML_IDENTIFIER} is (automatically) obtained by composing
+  \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}.
+  
+\item[\settdx{ISABELLE_PATH}*] is a list of directories (separated by colons)
+  where Isabelle logic images may reside. Note that the value of
+  \texttt{ML_IDENTIFIER} is appended to each component automatically.
 
 \item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
   files should be stored by default. The \texttt{ML_SYSTEM} identifier