Merge change 6922 into K5 (Poly users can omit -expk option).

Manual/Tutorial/intro.tex

@@ -127,15 +127,13 @@ \section{Installing HOL}
 into the \texttt{hol/bin} directory.  If something goes wrong at this
 stage, consult Section~\ref{sec:editting-configure} below.
 
-The next step is to run the \texttt{build} program.  When using
-Poly/ML, you must pass this program the \texttt{-expk} option. This
-should result in a great deal of output as all of the system code is
-compiled and the theories built.  Eventually, a \HOL{}
-system\footnote{Four \HOL{} executables are produced: \textsf{hol},
-  \textsf{hol.noquote}, \textsf{hol.bare} and
-  \textsf{hol.bare.noquote}.  The first of these will be used for most
-  examples in the \TUTORIAL{}.} is produced in the \texttt{bin/}
-directory.
+The next step is to run the \texttt{build} program.  This should
+result in a great deal of output as all of the system code is compiled
+and the theories built.  Eventually, a \HOL{} system\footnote{Four
+  \HOL{} executables are produced: \textsf{hol}, \textsf{hol.noquote},
+  \textsf{hol.bare} and \textsf{hol.bare.noquote}.  The first of these
+  will be used for most examples in the \TUTORIAL{}.} is produced in
+the \texttt{bin/} directory.
 
 \begin{session}
 \begin{alltt}

install.txt

@@ -117,7 +117,7 @@ C. In the HOL directory (<hol-dir>), type
 D. Now perform the following shell command:
 
        [Moscow ML:] <hol-dir>/bin/build
-       [Poly/ML:]   <hol-dir>/bin/build -expk
+       [Poly/ML:]   <hol-dir>/bin/build
 
    This builds the system. In case of difficulty, the configuration
    can be gone through by hand, by starting the ML interpreter and

tools-poly/build.sml

@@ -30,11 +30,14 @@ val DYNLIB = Systeml.DYNLIB
    ---------------------------------------------------------------------- *)
 
 
-(* use the experimental kernel? *)
+(* use the experimental kernel? - Yes!  Poly bug prevents use of standard
+   kernel *)
 val (use_expk, cmdline) =   let
-  val (expks, rest) = List.partition (fn e => e = "-expk") cmdline
+  val _ = print "** Using the experimental kernel (standard kernel \
+                \doesn't work with Poly/ML) **\n"
+  val (_, rest) = List.partition (fn e => e = "-expk") cmdline
 in
-  (not (null expks), rest)
+  (true, rest)
 end
 
 (* do self-tests? and to what level *)