1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Nov 20 00:53:26 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Nov 20 01:07:16 2010 +0100
     1.3 @@ -799,15 +799,15 @@
     1.4    \end{description}
     1.5  
     1.6    \paragraph{Historical note.} In the original SML90 standard the
     1.7 -  primitive ML type @{ML_type char} did not exists, and the basic @{ML
     1.8 +  primitive ML type @{ML_type char} did not exists, and the @{ML_text
     1.9    "explode: string -> string list"} operation would produce a list of
    1.10 -  singleton strings as in Isabelle/ML today.  When SML97 came out,
    1.11 -  Isabelle did not adopt its slightly anachronistic 8-bit characters,
    1.12 -  but the idea of exploding a string into a list of small strings was
    1.13 -  extended to ``symbols'' as explained above.  Thus Isabelle sources
    1.14 -  can refer to an infinite store of user-defined symbols, without
    1.15 -  having to worry about the multitude of Unicode encodings.
    1.16 -*}
    1.17 +  singleton strings as does @{ML "raw_explode: string -> string list"}
    1.18 +  in Isabelle/ML today.  When SML97 came out, Isabelle did not adopt
    1.19 +  its slightly anachronistic 8-bit characters, but the idea of
    1.20 +  exploding a string into a list of small strings was extended to
    1.21 +  ``symbols'' as explained above.  Thus Isabelle sources can refer to
    1.22 +  an infinite store of user-defined symbols, without having to worry
    1.23 +  about the multitude of Unicode encodings.  *}
    1.24  
    1.25  
    1.26  subsection {* Basic names \label{sec:basic-name} *}

     2.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Nov 20 00:53:26 2010 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Nov 20 01:07:16 2010 +0100
     2.3 @@ -1188,13 +1188,14 @@
     2.4    \end{description}
     2.5  
     2.6    \paragraph{Historical note.} In the original SML90 standard the
     2.7 -  primitive ML type \verb|char| did not exists, and the basic \verb|explode: string -> string list| operation would produce a list of
     2.8 -  singleton strings as in Isabelle/ML today.  When SML97 came out,
     2.9 -  Isabelle did not adopt its slightly anachronistic 8-bit characters,
    2.10 -  but the idea of exploding a string into a list of small strings was
    2.11 -  extended to ``symbols'' as explained above.  Thus Isabelle sources
    2.12 -  can refer to an infinite store of user-defined symbols, without
    2.13 -  having to worry about the multitude of Unicode encodings.%
    2.14 +  primitive ML type \verb|char| did not exists, and the \verb|explode: string -> string list| operation would produce a list of
    2.15 +  singleton strings as does \verb|raw_explode: string -> string list|
    2.16 +  in Isabelle/ML today.  When SML97 came out, Isabelle did not adopt
    2.17 +  its slightly anachronistic 8-bit characters, but the idea of
    2.18 +  exploding a string into a list of small strings was extended to
    2.19 +  ``symbols'' as explained above.  Thus Isabelle sources can refer to
    2.20 +  an infinite store of user-defined symbols, without having to worry
    2.21 +  about the multitude of Unicode encodings.%
    2.22  \end{isamarkuptext}%
    2.23  \isamarkuptrue%
    2.24  %