diff --git a/src/Doc/Implementation/ML.thy b/src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy
+++ b/src/Doc/Implementation/ML.thy
@@ -1,2211 +1,2229 @@
 (*:maxLineLen=78:*)
 
 theory "ML"
 imports Base
 begin
 
 chapter \<open>Isabelle/ML\<close>
 
 text \<open>
   Isabelle/ML is best understood as a certain culture based on Standard ML.
   Thus it is not a new programming language, but a certain way to use SML at
   an advanced level within the Isabelle environment. This covers a variety of
   aspects that are geared towards an efficient and robust platform for
   applications of formal logic with fully foundational proof construction ---
   according to the well-known \<^emph>\<open>LCF principle\<close>. There is specific
   infrastructure with library modules to address the needs of this difficult
   task. For example, the raw parallel programming model of Poly/ML is
   presented as considerably more abstract concept of \<^emph>\<open>futures\<close>, which is then
   used to augment the inference kernel, Isar theory and proof interpreter, and
   PIDE document management.
 
   The main aspects of Isabelle/ML are introduced below. These first-hand
   explanations should help to understand how proper Isabelle/ML is to be read
   and written, and to get access to the wealth of experience that is expressed
   in the source text and its history of changes.\<^footnote>\<open>See
   \<^url>\<open>https://isabelle.in.tum.de/repos/isabelle\<close> for the full Mercurial history.
   There are symbolic tags to refer to official Isabelle releases, as opposed
   to arbitrary \<^emph>\<open>tip\<close> versions that merely reflect snapshots that are never
   really up-to-date.\<close>
 \<close>
 
 
 section \<open>Style and orthography\<close>
 
 text \<open>
   The sources of Isabelle/Isar are optimized for \<^emph>\<open>readability\<close> and
   \<^emph>\<open>maintainability\<close>. The main purpose is to tell an informed reader what is
   really going on and how things really work. This is a non-trivial aim, but
   it is supported by a certain style of writing Isabelle/ML that has emerged
   from long years of system development.\<^footnote>\<open>See also the interesting style guide
   for OCaml \<^url>\<open>https://caml.inria.fr/resources/doc/guides/guidelines.en.html\<close>
   which shares many of our means and ends.\<close>
 
   The main principle behind any coding style is \<^emph>\<open>consistency\<close>. For a single
   author of a small program this merely means ``choose your style and stick to
   it''. A complex project like Isabelle, with long years of development and
   different contributors, requires more standardization. A coding style that
   is changed every few years or with every new contributor is no style at all,
   because consistency is quickly lost. Global consistency is hard to achieve,
   though. Nonetheless, one should always strive at least for local consistency
   of modules and sub-systems, without deviating from some general principles
   how to write Isabelle/ML.
 
   In a sense, good coding style is like an \<^emph>\<open>orthography\<close> for the sources: it
   helps to read quickly over the text and see through the main points, without
   getting distracted by accidental presentation of free-style code.
 \<close>
 
 
 subsection \<open>Header and sectioning\<close>
 
 text \<open>
   Isabelle source files have a certain standardized header format (with
   precise spacing) that follows ancient traditions reaching back to the
   earliest versions of the system by Larry Paulson. See
   \<^file>\<open>~~/src/Pure/thm.ML\<close>, for example.
 
   The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries, followed by a
   prose description of the purpose of the module. The latter can range from a
   single line to several paragraphs of explanations.
 
   The rest of the file is divided into chapters, sections, subsections,
   subsubsections, paragraphs etc.\ using a simple layout via ML comments as
   follows.
 
   @{verbatim [display]
 \<open>  (**** chapter ****)
  
   (*** section ***)
 
   (** subsection **)
 
   (* subsubsection *)
 
   (*short paragraph*)
 
   (*
     long paragraph,
     with more text
   *)\<close>}
 
   As in regular typography, there is some extra space \<^emph>\<open>before\<close> section
   headings that are adjacent to plain text, but not other headings as in the
   example above.
 
   \<^medskip>
   The precise wording of the prose text given in these headings is chosen
   carefully to introduce the main theme of the subsequent formal ML text.
 \<close>
 
 
 subsection \<open>Naming conventions\<close>
 
 text \<open>
   Since ML is the primary medium to express the meaning of the source text,
   naming of ML entities requires special care.
 \<close>
 
 paragraph \<open>Notation.\<close>
 text \<open>
   A name consists of 1--3 \<^emph>\<open>words\<close> (rarely 4, but not more) that are separated
   by underscore. There are three variants concerning upper or lower case
   letters, which are used for certain ML categories as follows:
 
   \<^medskip>
   \begin{tabular}{lll}
   variant & example & ML categories \\\hline
   lower-case & \<^ML_text>\<open>foo_bar\<close> & values, types, record fields \\
   capitalized & \<^ML_text>\<open>Foo_Bar\<close> & datatype constructors, structures, functors \\
   upper-case & \<^ML_text>\<open>FOO_BAR\<close> & special values, exception constructors, signatures \\
   \end{tabular}
   \<^medskip>
 
   For historical reasons, many capitalized names omit underscores, e.g.\
   old-style \<^ML_text>\<open>FooBar\<close> instead of \<^ML_text>\<open>Foo_Bar\<close>. Genuine
   mixed-case names are \<^emph>\<open>not\<close> used, because clear division of words is
   essential for readability.\<^footnote>\<open>Camel-case was invented to workaround the lack
   of underscore in some early non-ASCII character sets. Later it became
   habitual in some language communities that are now strong in numbers.\<close>
 
   A single (capital) character does not count as ``word'' in this respect:
   some Isabelle/ML names are suffixed by extra markers like this: \<^ML_text>\<open>foo_barT\<close>.
 
   Name variants are produced by adding 1--3 primes, e.g.\ \<^ML_text>\<open>foo'\<close>,
   \<^ML_text>\<open>foo''\<close>, or \<^ML_text>\<open>foo'''\<close>, but not \<^ML_text>\<open>foo''''\<close> or more.
   Decimal digits scale better to larger numbers, e.g.\ \<^ML_text>\<open>foo0\<close>,
   \<^ML_text>\<open>foo1\<close>, \<^ML_text>\<open>foo42\<close>.
 \<close>
 
 paragraph \<open>Scopes.\<close>
 text \<open>
   Apart from very basic library modules, ML structures are not ``opened'', but
-  names are referenced with explicit qualification, as in \<^ML>\<open>Syntax.string_of_term\<close> for example. When devising names for structures and
-  their components it is important to aim at eye-catching compositions of both
-  parts, because this is how they are seen in the sources and documentation.
-  For the same reasons, aliases of well-known library functions should be
-  avoided.
+  names are referenced with explicit qualification, as in
+  \<^ML>\<open>Syntax.string_of_term\<close> for example. When devising names for
+  structures and their components it is important to aim at eye-catching
+  compositions of both parts, because this is how they are seen in the sources
+  and documentation. For the same reasons, aliases of well-known library
+  functions should be avoided.
 
   Local names of function abstraction or case/let bindings are typically
   shorter, sometimes using only rudiments of ``words'', while still avoiding
   cryptic shorthands. An auxiliary function called \<^ML_text>\<open>helper\<close>,
   \<^ML_text>\<open>aux\<close>, or \<^ML_text>\<open>f\<close> is considered bad style.
 
   Example:
 
   @{verbatim [display]
 \<open>  (* RIGHT *)
 
   fun print_foo ctxt foo =
     let
       fun print t = ... Syntax.string_of_term ctxt t ...
     in ... end;
 
 
   (* RIGHT *)
 
   fun print_foo ctxt foo =
     let
       val string_of_term = Syntax.string_of_term ctxt;
       fun print t = ... string_of_term t ...
     in ... end;
 
 
   (* WRONG *)
 
   val string_of_term = Syntax.string_of_term;
 
   fun print_foo ctxt foo =
     let
       fun aux t = ... string_of_term ctxt t ...
     in ... end;\<close>}
 \<close>
 
 paragraph \<open>Specific conventions.\<close>
 text \<open>
   Here are some specific name forms that occur frequently in the sources.
 
-  \<^item> A function that maps \<^ML_text>\<open>foo\<close> to \<^ML_text>\<open>bar\<close> is called \<^ML_text>\<open>foo_to_bar\<close> or \<^ML_text>\<open>bar_of_foo\<close> (never \<^ML_text>\<open>foo2bar\<close>, nor
-  \<^ML_text>\<open>bar_from_foo\<close>, nor \<^ML_text>\<open>bar_for_foo\<close>, nor \<^ML_text>\<open>bar4foo\<close>).
+  \<^item> A function that maps \<^ML_text>\<open>foo\<close> to \<^ML_text>\<open>bar\<close> is called
+  \<^ML_text>\<open>foo_to_bar\<close> or \<^ML_text>\<open>bar_of_foo\<close> (never
+  \<^ML_text>\<open>foo2bar\<close>, nor \<^ML_text>\<open>bar_from_foo\<close>, nor
+  \<^ML_text>\<open>bar_for_foo\<close>, nor \<^ML_text>\<open>bar4foo\<close>).
 
   \<^item> The name component \<^ML_text>\<open>legacy\<close> means that the operation is about to
   be discontinued soon.
 
   \<^item> The name component \<^ML_text>\<open>global\<close> means that this works with the
   background theory instead of the regular local context
   (\secref{sec:context}), sometimes for historical reasons, sometimes due a
   genuine lack of locality of the concept involved, sometimes as a fall-back
   for the lack of a proper context in the application code. Whenever there is
   a non-global variant available, the application should be migrated to use it
   with a proper local context.
 
   \<^item> Variables of the main context types of the Isabelle/Isar framework
   (\secref{sec:context} and \chref{ch:local-theory}) have firm naming
   conventions as follows:
 
     \<^item> theories are called \<^ML_text>\<open>thy\<close>, rarely \<^ML_text>\<open>theory\<close>
     (never \<^ML_text>\<open>thry\<close>)
 
-    \<^item> proof contexts are called \<^ML_text>\<open>ctxt\<close>, rarely \<^ML_text>\<open>context\<close> (never \<^ML_text>\<open>ctx\<close>)
+    \<^item> proof contexts are called \<^ML_text>\<open>ctxt\<close>, rarely \<^ML_text>\<open>context\<close>
+    (never \<^ML_text>\<open>ctx\<close>)
 
     \<^item> generic contexts are called \<^ML_text>\<open>context\<close>
 
     \<^item> local theories are called \<^ML_text>\<open>lthy\<close>, except for local
     theories that are treated as proof context (which is a semantic
     super-type)
 
   Variations with primed or decimal numbers are always possible, as well as
   semantic prefixes like \<^ML_text>\<open>foo_thy\<close> or \<^ML_text>\<open>bar_ctxt\<close>, but the
   base conventions above need to be preserved. This allows to emphasize their
   data flow via plain regular expressions in the text editor.
 
   \<^item> The main logical entities (\secref{ch:logic}) have established naming
   convention as follows:
 
     \<^item> sorts are called \<^ML_text>\<open>S\<close>
 
     \<^item> types are called \<^ML_text>\<open>T\<close>, \<^ML_text>\<open>U\<close>, or \<^ML_text>\<open>ty\<close> (never
     \<^ML_text>\<open>t\<close>)
 
     \<^item> terms are called \<^ML_text>\<open>t\<close>, \<^ML_text>\<open>u\<close>, or \<^ML_text>\<open>tm\<close> (never
     \<^ML_text>\<open>trm\<close>)
 
     \<^item> certified types are called \<^ML_text>\<open>cT\<close>, rarely \<^ML_text>\<open>T\<close>, with
     variants as for types
 
     \<^item> certified terms are called \<^ML_text>\<open>ct\<close>, rarely \<^ML_text>\<open>t\<close>, with
     variants as for terms (never \<^ML_text>\<open>ctrm\<close>)
 
     \<^item> theorems are called \<^ML_text>\<open>th\<close>, or \<^ML_text>\<open>thm\<close>
 
   Proper semantic names override these conventions completely. For example,
   the left-hand side of an equation (as a term) can be called \<^ML_text>\<open>lhs\<close>
   (not \<^ML_text>\<open>lhs_tm\<close>). Or a term that is known to be a variable can be
   called \<^ML_text>\<open>v\<close> or \<^ML_text>\<open>x\<close>.
 
   \<^item> Tactics (\secref{sec:tactics}) are sufficiently important to have specific
   naming conventions. The name of a basic tactic definition always has a
   \<^ML_text>\<open>_tac\<close> suffix, the subgoal index (if applicable) is always called
   \<^ML_text>\<open>i\<close>, and the goal state (if made explicit) is usually called
   \<^ML_text>\<open>st\<close> instead of the somewhat misleading \<^ML_text>\<open>thm\<close>. Any other
   arguments are given before the latter two, and the general context is given
   first. Example:
 
   @{verbatim [display] \<open>  fun my_tac ctxt arg1 arg2 i st = ...\<close>}
 
   Note that the goal state \<^ML_text>\<open>st\<close> above is rarely made explicit, if
   tactic combinators (tacticals) are used as usual.
 
   A tactic that requires a proof context needs to make that explicit as seen
   in the \<^verbatim>\<open>ctxt\<close> argument above. Do not refer to the background theory of
   \<^verbatim>\<open>st\<close> -- it is not a proper context, but merely a formal certificate.
 \<close>
 
 
 subsection \<open>General source layout\<close>
 
 text \<open>
   The general Isabelle/ML source layout imitates regular type-setting
   conventions, augmented by the requirements for deeply nested expressions
   that are commonplace in functional programming.
 \<close>
 
 paragraph \<open>Line length\<close>
 text \<open>
   is limited to 80 characters according to ancient standards, but we allow as
   much as 100 characters (not more).\<^footnote>\<open>Readability requires to keep the
   beginning of a line in view while watching its end. Modern wide-screen
   displays do not change the way how the human brain works. Sources also need
   to be printable on plain paper with reasonable font-size.\<close> The extra 20
   characters acknowledge the space requirements due to qualified library
   references in Isabelle/ML.
 \<close>
 
 paragraph \<open>White-space\<close>
 text \<open>
   is used to emphasize the structure of expressions, following mostly standard
   conventions for mathematical typesetting, as can be seen in plain {\TeX} or
   {\LaTeX}. This defines positioning of spaces for parentheses, punctuation,
   and infixes as illustrated here:
 
   @{verbatim [display]
 \<open>  val x = y + z * (a + b);
   val pair = (a, b);
   val record = {foo = 1, bar = 2};\<close>}
 
   Lines are normally broken \<^emph>\<open>after\<close> an infix operator or punctuation
   character. For example:
 
   @{verbatim [display]
 \<open>
   val x =
     a +
     b +
     c;
 
   val tuple =
    (a,
     b,
     c);
 \<close>}
 
   Some special infixes (e.g.\ \<^ML_text>\<open>|>\<close>) work better at the start of the
   line, but punctuation is always at the end.
 
   Function application follows the tradition of \<open>\<lambda>\<close>-calculus, not informal
   mathematics. For example: \<^ML_text>\<open>f a b\<close> for a curried function, or
   \<^ML_text>\<open>g (a, b)\<close> for a tupled function. Note that the space between
   \<^ML_text>\<open>g\<close> and the pair \<^ML_text>\<open>(a, b)\<close> follows the important
   principle of \<^emph>\<open>compositionality\<close>: the layout of \<^ML_text>\<open>g p\<close> does not
   change when \<^ML_text>\<open>p\<close> is refined to the concrete pair \<^ML_text>\<open>(a,
   b)\<close>.
 \<close>
 
 paragraph \<open>Indentation\<close>
 text \<open>
   uses plain spaces, never hard tabulators.\<^footnote>\<open>Tabulators were invented to move
   the carriage of a type-writer to certain predefined positions. In software
   they could be used as a primitive run-length compression of consecutive
   spaces, but the precise result would depend on non-standardized text editor
   configuration.\<close>
 
   Each level of nesting is indented by 2 spaces, sometimes 1, very rarely 4,
   never 8 or any other odd number.
 
   Indentation follows a simple logical format that only depends on the nesting
   depth, not the accidental length of the text that initiates a level of
   nesting. Example:
 
   @{verbatim [display]
 \<open>  (* RIGHT *)
 
   if b then
     expr1_part1
     expr1_part2
   else
     expr2_part1
     expr2_part2
 
 
   (* WRONG *)
 
   if b then expr1_part1
             expr1_part2
   else expr2_part1
        expr2_part2\<close>}
 
   The second form has many problems: it assumes a fixed-width font when
   viewing the sources, it uses more space on the line and thus makes it hard
   to observe its strict length limit (working against \<^emph>\<open>readability\<close>), it
   requires extra editing to adapt the layout to changes of the initial text
   (working against \<^emph>\<open>maintainability\<close>) etc.
 
   \<^medskip>
   For similar reasons, any kind of two-dimensional or tabular layouts,
   ASCII-art with lines or boxes of asterisks etc.\ should be avoided.
 \<close>
 
 paragraph \<open>Complex expressions\<close>
 text \<open>
   that consist of multi-clausal function definitions, \<^ML_text>\<open>handle\<close>,
   \<^ML_text>\<open>case\<close>, \<^ML_text>\<open>let\<close> (and combinations) require special
   attention. The syntax of Standard ML is quite ambitious and admits a lot of
   variance that can distort the meaning of the text.
 
   Multiple clauses of \<^ML_text>\<open>fun\<close>, \<^ML_text>\<open>fn\<close>, \<^ML_text>\<open>handle\<close>,
   \<^ML_text>\<open>case\<close> get extra indentation to indicate the nesting clearly.
   Example:
 
   @{verbatim [display]
 \<open>  (* RIGHT *)
 
   fun foo p1 =
         expr1
     | foo p2 =
         expr2
 
 
   (* WRONG *)
 
   fun foo p1 =
     expr1
     | foo p2 =
     expr2\<close>}
 
   Body expressions consisting of \<^ML_text>\<open>case\<close> or \<^ML_text>\<open>let\<close> require
   care to maintain compositionality, to prevent loss of logical indentation
   where it is especially important to see the structure of the text. Example:
 
   @{verbatim [display]
 \<open>  (* RIGHT *)
 
   fun foo p1 =
         (case e of
           q1 => ...
         | q2 => ...)
     | foo p2 =
         let
           ...
         in
           ...
         end
 
 
   (* WRONG *)
 
   fun foo p1 = case e of
       q1 => ...
     | q2 => ...
     | foo p2 =
     let
       ...
     in
       ...
     end\<close>}
 
   Extra parentheses around \<^ML_text>\<open>case\<close> expressions are optional, but help
   to analyse the nesting based on character matching in the text editor.
 
   \<^medskip>
   There are two main exceptions to the overall principle of compositionality
   in the layout of complex expressions.
 
   \<^enum> \<^ML_text>\<open>if\<close> expressions are iterated as if ML had multi-branch
   conditionals, e.g.
 
   @{verbatim [display]
 \<open>  (* RIGHT *)
 
   if b1 then e1
   else if b2 then e2
   else e3\<close>}
 
   \<^enum> \<^ML_text>\<open>fn\<close> abstractions are often layed-out as if they would lack any
   structure by themselves. This traditional form is motivated by the
   possibility to shift function arguments back and forth wrt.\ additional
   combinators. Example:
 
   @{verbatim [display]
 \<open>  (* RIGHT *)
 
   fun foo x y = fold (fn z =>
     expr)\<close>}
 
   Here the visual appearance is that of three arguments \<^ML_text>\<open>x\<close>,
   \<^ML_text>\<open>y\<close>, \<^ML_text>\<open>z\<close> in a row.
 
 
   Such weakly structured layout should be use with great care. Here are some
   counter-examples involving \<^ML_text>\<open>let\<close> expressions:
 
   @{verbatim [display]
 \<open>  (* WRONG *)
 
   fun foo x = let
       val y = ...
     in ... end
 
 
   (* WRONG *)
 
   fun foo x = let
     val y = ...
   in ... end
 
 
   (* WRONG *)
 
   fun foo x =
   let
     val y = ...
   in ... end
 
 
   (* WRONG *)
 
   fun foo x =
     let
       val y = ...
     in
       ... end\<close>}
 
   \<^medskip>
   In general the source layout is meant to emphasize the structure of complex
   language expressions, not to pretend that SML had a completely different
   syntax (say that of Haskell, Scala, Java).
 \<close>
 
 
 section \<open>ML embedded into Isabelle/Isar\<close>
 
 text \<open>
   ML and Isar are intertwined via an open-ended bootstrap process that
   provides more and more programming facilities and logical content in an
   alternating manner. Bootstrapping starts from the raw environment of
   existing implementations of Standard ML (mainly Poly/ML).
 
   Isabelle/Pure marks the point where the raw ML toplevel is superseded by
   Isabelle/ML within the Isar theory and proof language, with a uniform
   context for arbitrary ML values (see also \secref{sec:context}). This formal
   environment holds ML compiler bindings, logical entities, and many other
   things.
 
   Object-logics like Isabelle/HOL are built within the Isabelle/ML/Isar
   environment by introducing suitable theories with associated ML modules,
   either inlined within \<^verbatim>\<open>.thy\<close> files, or as separate \<^verbatim>\<open>.ML\<close> files that are
   loading from some theory. Thus Isabelle/HOL is defined as a regular
   user-space application within the Isabelle framework. Further add-on tools
   can be implemented in ML within the Isar context in the same manner: ML is
   part of the standard repertoire of Isabelle, and there is no distinction
   between ``users'' and ``developers'' in this respect.
 \<close>
 
 
 subsection \<open>Isar ML commands\<close>
 
 text \<open>
   The primary Isar source language provides facilities to ``open a window'' to
   the underlying ML compiler. Especially see the Isar commands @{command_ref
   "ML_file"} and @{command_ref "ML"}: both work the same way, but the source
   text is provided differently, via a file vs.\ inlined, respectively. Apart
   from embedding ML into the main theory definition like that, there are many
   more commands that refer to ML source, such as @{command_ref setup} or
   @{command_ref declaration}. Even more fine-grained embedding of ML into Isar
   is encountered in the proof method @{method_ref tactic}, which refines the
   pending goal state via a given expression of type \<^ML_type>\<open>tactic\<close>.
 \<close>
 
 text %mlex \<open>
   The following artificial example demonstrates some ML toplevel declarations
   within the implicit Isar theory context. This is regular functional
   programming without referring to logical entities yet.
 \<close>
 
 ML \<open>
   fun factorial 0 = 1
     | factorial n = n * factorial (n - 1)
 \<close>
 
 text \<open>
-  Here the ML environment is already managed by Isabelle, i.e.\ the \<^ML>\<open>factorial\<close> function is not yet accessible in the preceding paragraph, nor in
-  a different theory that is independent from the current one in the import
-  hierarchy.
+  Here the ML environment is already managed by Isabelle, i.e.\ the
+  \<^ML>\<open>factorial\<close> function is not yet accessible in the preceding paragraph,
+  nor in a different theory that is independent from the current one in the
+  import hierarchy.
 
   Removing the above ML declaration from the source text will remove any trace
   of this definition, as expected. The Isabelle/ML toplevel environment is
   managed in a \<^emph>\<open>stateless\<close> way: in contrast to the raw ML toplevel, there are
   no global side-effects involved here.\<^footnote>\<open>Such a stateless compilation
   environment is also a prerequisite for robust parallel compilation within
   independent nodes of the implicit theory development graph.\<close>
 
   \<^medskip>
   The next example shows how to embed ML into Isar proofs, using @{command_ref
   "ML_prf"} instead of @{command_ref "ML"}. As illustrated below, the effect
   on the ML environment is local to the whole proof body, but ignoring the
   block structure.
 \<close>
 
 notepad
 begin
   ML_prf %"ML" \<open>val a = 1\<close>
   {
     ML_prf %"ML" \<open>val b = a + 1\<close>
   } \<comment> \<open>Isar block structure ignored by ML environment\<close>
   ML_prf %"ML" \<open>val c = b + 1\<close>
 end
 
 text \<open>
   By side-stepping the normal scoping rules for Isar proof blocks, embedded ML
   code can refer to the different contexts and manipulate corresponding
   entities, e.g.\ export a fact from a block context.
 
   \<^medskip>
   Two further ML commands are useful in certain situations: @{command_ref
   ML_val} and @{command_ref ML_command} are \<^emph>\<open>diagnostic\<close> in the sense that
   there is no effect on the underlying environment, and can thus be used
-  anywhere. The examples below produce long strings of digits by invoking \<^ML>\<open>factorial\<close>: @{command ML_val} takes care of printing the ML toplevel result,
-  but @{command ML_command} is silent so we produce an explicit output
+  anywhere. The examples below produce long strings of digits by invoking
+  \<^ML>\<open>factorial\<close>: @{command ML_val} takes care of printing the ML toplevel
+  result, but @{command ML_command} is silent so we produce an explicit output
   message.
 \<close>
 
 ML_val \<open>factorial 100\<close>
 ML_command \<open>writeln (string_of_int (factorial 100))\<close>
 
 notepad
 begin
   ML_val \<open>factorial 100\<close>
   ML_command \<open>writeln (string_of_int (factorial 100))\<close>
 end
 
 
 subsection \<open>Compile-time context\<close>
 
 text \<open>
   Whenever the ML compiler is invoked within Isabelle/Isar, the formal context
   is passed as a thread-local reference variable. Thus ML code may access the
   theory context during compilation, by reading or writing the (local) theory
   under construction. Note that such direct access to the compile-time context
   is rare. In practice it is typically done via some derived ML functions
   instead.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML Context.the_generic_context: "unit -> Context.generic"} \\
   @{define_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
   @{define_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
   @{define_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
   \end{mldecls}
 
     \<^descr> \<^ML>\<open>Context.the_generic_context ()\<close> refers to the theory context of
     the ML toplevel --- at compile time. ML code needs to take care to refer to
     \<^ML>\<open>Context.the_generic_context ()\<close> correctly. Recall that evaluation
     of a function body is delayed until actual run-time.
 
     \<^descr> \<^ML>\<open>Context.>>\<close>~\<open>f\<close> applies context transformation \<open>f\<close> to the implicit
     context of the ML toplevel.
 
     \<^descr> \<^ML>\<open>ML_Thms.bind_thms\<close>~\<open>(name, thms)\<close> stores a list of theorems produced
     in ML both in the (global) theory context and the ML toplevel, associating
     it with the provided name.
 
     \<^descr> \<^ML>\<open>ML_Thms.bind_thm\<close> is similar to \<^ML>\<open>ML_Thms.bind_thms\<close> but refers to
     a singleton fact.
 
   It is important to note that the above functions are really restricted to
   the compile time, even though the ML compiler is invoked at run-time. The
   majority of ML code either uses static antiquotations
   (\secref{sec:ML-antiq}) or refers to the theory or proof context at
   run-time, by explicit functional abstraction.
 \<close>
 
 
 subsection \<open>Antiquotations \label{sec:ML-antiq}\<close>
 
 text \<open>
   A very important consequence of embedding ML into Isar is the concept of
   \<^emph>\<open>ML antiquotation\<close>. The standard token language of ML is augmented by
   special syntactic entities of the following form:
 
   \<^rail>\<open>
   @{syntax_def antiquote}: '@{' name args '}'
   \<close>
 
   Here @{syntax name} and @{syntax args} are outer syntax categories, as
   defined in @{cite "isabelle-isar-ref"}.
 
   \<^medskip>
   A regular antiquotation \<open>@{name args}\<close> processes its arguments by the usual
   means of the Isar source language, and produces corresponding ML source
   text, either as literal \<^emph>\<open>inline\<close> text (e.g.\ \<open>@{term t}\<close>) or abstract
   \<^emph>\<open>value\<close> (e.g. \<open>@{thm th}\<close>). This pre-compilation scheme allows to refer to
   formal entities in a robust manner, with proper static scoping and with some
   degree of logical checking of small portions of the code.
 \<close>
 
 
 subsection \<open>Printing ML values\<close>
 
 text \<open>
   The ML compiler knows about the structure of values according to their
   static type, and can print them in the manner of its toplevel, although the
   details are non-portable. The antiquotations @{ML_antiquotation_def
   "make_string"} and @{ML_antiquotation_def "print"} provide a quasi-portable
   way to refer to this potential capability of the underlying ML system in
   generic Isabelle/ML sources.
 
   This is occasionally useful for diagnostic or demonstration purposes. Note
   that production-quality tools require proper user-level error messages,
   avoiding raw ML values in the output.
 \<close>
 
 text %mlantiq \<open>
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "make_string"} & : & \<open>ML_antiquotation\<close> \\
   @{ML_antiquotation_def "print"} & : & \<open>ML_antiquotation\<close> \\
   \end{matharray}
 
   \<^rail>\<open>
   @@{ML_antiquotation make_string}
   ;
   @@{ML_antiquotation print} embedded?
   \<close>
 
   \<^descr> \<open>@{make_string}\<close> inlines a function to print arbitrary values similar to
   the ML toplevel. The result is compiler dependent and may fall back on "?"
   in certain situations. The value of configuration option @{attribute_ref
   ML_print_depth} determines further details of output.
 
   \<^descr> \<open>@{print f}\<close> uses the ML function \<open>f: string -> unit\<close> to output the result
   of \<open>@{make_string}\<close> above, together with the source position of the
   antiquotation. The default output function is \<^ML>\<open>writeln\<close>.
 \<close>
 
 text %mlex \<open>
   The following artificial examples show how to produce adhoc output of ML
   values for debugging purposes.
 \<close>
 
 ML_val \<open>
   val x = 42;
   val y = true;
 
   writeln (\<^make_string> {x = x, y = y});
 
   \<^print> {x = x, y = y};
   \<^print>\<open>tracing\<close> {x = x, y = y};
 \<close>
 
 
 section \<open>Canonical argument order \label{sec:canonical-argument-order}\<close>
 
 text \<open>
   Standard ML is a language in the tradition of \<open>\<lambda>\<close>-calculus and
   \<^emph>\<open>higher-order functional programming\<close>, similar to OCaml, Haskell, or
   Isabelle/Pure and HOL as logical languages. Getting acquainted with the
   native style of representing functions in that setting can save a lot of
   extra boiler-plate of redundant shuffling of arguments, auxiliary
   abstractions etc.
 
   Functions are usually \<^emph>\<open>curried\<close>: the idea of turning arguments of type
   \<open>\<tau>\<^sub>i\<close> (for \<open>i \<in> {1, \<dots> n}\<close>) into a result of type \<open>\<tau>\<close> is represented by the
   iterated function space \<open>\<tau>\<^sub>1 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>\<close>. This is isomorphic to the
   well-known encoding via tuples \<open>\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<rightarrow> \<tau>\<close>, but the curried version
   fits more smoothly into the basic calculus.\<^footnote>\<open>The difference is even more
   significant in HOL, because the redundant tuple structure needs to be
   accommodated extraneous proof steps.\<close>
 
   Currying gives some flexibility due to \<^emph>\<open>partial application\<close>. A function
   \<open>f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<tau>\<close> can be applied to \<open>x: \<tau>\<^sub>1\<close> and the remaining \<open>(f x): \<tau>\<^sub>2
   \<rightarrow> \<tau>\<close> passed to another function etc. How well this works in practice depends
   on the order of arguments. In the worst case, arguments are arranged
   erratically, and using a function in a certain situation always requires
   some glue code. Thus we would get exponentially many opportunities to
   decorate the code with meaningless permutations of arguments.
 
   This can be avoided by \<^emph>\<open>canonical argument order\<close>, which observes certain
   standard patterns and minimizes adhoc permutations in their application. In
   Isabelle/ML, large portions of text can be written without auxiliary
   operations like \<open>swap: \<alpha> \<times> \<beta> \<rightarrow> \<beta> \<times> \<alpha>\<close> or \<open>C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)\<close> (the
   latter is not present in the Isabelle/ML library).
 
   \<^medskip>
   The main idea is that arguments that vary less are moved further to the left
   than those that vary more. Two particularly important categories of
   functions are \<^emph>\<open>selectors\<close> and \<^emph>\<open>updates\<close>.
 
   The subsequent scheme is based on a hypothetical set-like container of type
   \<open>\<beta>\<close> that manages elements of type \<open>\<alpha>\<close>. Both the names and types of the
   associated operations are canonical for Isabelle/ML.
 
   \begin{center}
   \begin{tabular}{ll}
   kind & canonical name and type \\\hline
   selector & \<open>member: \<beta> \<rightarrow> \<alpha> \<rightarrow> bool\<close> \\
   update & \<open>insert: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>\<close> \\
   \end{tabular}
   \end{center}
 
   Given a container \<open>B: \<beta>\<close>, the partially applied \<open>member B\<close> is a predicate
   over elements \<open>\<alpha> \<rightarrow> bool\<close>, and thus represents the intended denotation
   directly. It is customary to pass the abstract predicate to further
   operations, not the concrete container. The argument order makes it easy to
   use other combinators: \<open>forall (member B) list\<close> will check a list of
   elements for membership in \<open>B\<close> etc. Often the explicit \<open>list\<close> is pointless
   and can be contracted to \<open>forall (member B)\<close> to get directly a predicate
   again.
 
   In contrast, an update operation varies the container, so it moves to the
   right: \<open>insert a\<close> is a function \<open>\<beta> \<rightarrow> \<beta>\<close> to insert a value \<open>a\<close>. These can be
   composed naturally as \<open>insert c \<circ> insert b \<circ> insert a\<close>. The slightly awkward
   inversion of the composition order is due to conventional mathematical
   notation, which can be easily amended as explained below.
 \<close>
 
 
 subsection \<open>Forward application and composition\<close>
 
 text \<open>
   Regular function application and infix notation works best for relatively
   deeply structured expressions, e.g.\ \<open>h (f x y + g z)\<close>. The important
   special case of \<^emph>\<open>linear transformation\<close> applies a cascade of functions \<open>f\<^sub>n
   (\<dots> (f\<^sub>1 x))\<close>. This becomes hard to read and maintain if the functions are
   themselves given as complex expressions. The notation can be significantly
   improved by introducing \<^emph>\<open>forward\<close> versions of application and composition
   as follows:
 
   \<^medskip>
   \begin{tabular}{lll}
   \<open>x |> f\<close> & \<open>\<equiv>\<close> & \<open>f x\<close> \\
   \<open>(f #> g) x\<close> & \<open>\<equiv>\<close> & \<open>x |> f |> g\<close> \\
   \end{tabular}
   \<^medskip>
 
   This enables to write conveniently \<open>x |> f\<^sub>1 |> \<dots> |> f\<^sub>n\<close> or \<open>f\<^sub>1 #> \<dots> #>
   f\<^sub>n\<close> for its functional abstraction over \<open>x\<close>.
 
   \<^medskip>
   There is an additional set of combinators to accommodate multiple results
   (via pairs) that are passed on as multiple arguments (via currying).
 
   \<^medskip>
   \begin{tabular}{lll}
   \<open>(x, y) |-> f\<close> & \<open>\<equiv>\<close> & \<open>f x y\<close> \\
   \<open>(f #-> g) x\<close> & \<open>\<equiv>\<close> & \<open>x |> f |-> g\<close> \\
   \end{tabular}
   \<^medskip>
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_infix "|>" : "'a * ('a -> 'b) -> 'b"} \\
   @{define_ML_infix "|->" : "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
   @{define_ML_infix "#>" : "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
   @{define_ML_infix "#->" : "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
   \end{mldecls}
 \<close>
 
 
 subsection \<open>Canonical iteration\<close>
 
 text \<open>
   As explained above, a function \<open>f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>\<close> can be understood as update on
   a configuration of type \<open>\<beta>\<close>, parameterized by an argument of type \<open>\<alpha>\<close>. Given
   \<open>a: \<alpha>\<close> the partial application \<open>(f a): \<beta> \<rightarrow> \<beta>\<close> operates homogeneously on \<open>\<beta>\<close>.
   This can be iterated naturally over a list of parameters \<open>[a\<^sub>1, \<dots>, a\<^sub>n]\<close> as
   \<open>f a\<^sub>1 #> \<dots> #> f a\<^sub>n\<close>. The latter expression is again a function \<open>\<beta> \<rightarrow> \<beta>\<close>. It
   can be applied to an initial configuration \<open>b: \<beta>\<close> to start the iteration
   over the given list of arguments: each \<open>a\<close> in \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> is applied
   consecutively by updating a cumulative configuration.
 
   The \<open>fold\<close> combinator in Isabelle/ML lifts a function \<open>f\<close> as above to its
   iterated version over a list of arguments. Lifting can be repeated, e.g.\
   \<open>(fold \<circ> fold) f\<close> iterates over a list of lists as expected.
 
   The variant \<open>fold_rev\<close> works inside-out over the list of arguments, such
   that \<open>fold_rev f \<equiv> fold f \<circ> rev\<close> holds.
 
   The \<open>fold_map\<close> combinator essentially performs \<open>fold\<close> and \<open>map\<close>
   simultaneously: each application of \<open>f\<close> produces an updated configuration
   together with a side-result; the iteration collects all such side-results as
   a separate list.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
   @{define_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
   @{define_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>fold\<close>~\<open>f\<close> lifts the parametrized update function \<open>f\<close> to a list of
   parameters.
 
   \<^descr> \<^ML>\<open>fold_rev\<close>~\<open>f\<close> is similar to \<^ML>\<open>fold\<close>~\<open>f\<close>, but works inside-out, as
   if the list would be reversed.
 
   \<^descr> \<^ML>\<open>fold_map\<close>~\<open>f\<close> lifts the parametrized update function \<open>f\<close> (with
   side-result) to a list of parameters and cumulative side-results.
 
 
   \begin{warn}
   The literature on functional programming provides a confusing multitude of
   combinators called \<open>foldl\<close>, \<open>foldr\<close> etc. SML97 provides its own variations
   as \<^ML>\<open>List.foldl\<close> and \<^ML>\<open>List.foldr\<close>, while the classic Isabelle library
   also has the historic \<^ML>\<open>Library.foldl\<close> and \<^ML>\<open>Library.foldr\<close>. To avoid
   unnecessary complication, all these historical versions should be ignored,
   and the canonical \<^ML>\<open>fold\<close> (or \<^ML>\<open>fold_rev\<close>) used exclusively.
   \end{warn}
 \<close>
 
 text %mlex \<open>
   The following example shows how to fill a text buffer incrementally by
   adding strings, either individually or from a given list.
 \<close>
 
 ML_val \<open>
   val s =
     Buffer.empty
     |> Buffer.add "digits: "
     |> fold (Buffer.add o string_of_int) (0 upto 9)
     |> Buffer.content;
 
   \<^assert> (s = "digits: 0123456789");
 \<close>
 
 text \<open>
-  Note how \<^ML>\<open>fold (Buffer.add o string_of_int)\<close> above saves an extra \<^ML>\<open>map\<close> over the given list. This kind of peephole optimization reduces both
-  the code size and the tree structures in memory (``deforestation''), but it
-  requires some practice to read and write fluently.
+  Note how \<^ML>\<open>fold (Buffer.add o string_of_int)\<close> above saves an extra
+  \<^ML>\<open>map\<close> over the given list. This kind of peephole optimization reduces
+  both the code size and the tree structures in memory (``deforestation''),
+  but it requires some practice to read and write fluently.
 
   \<^medskip>
   The next example elaborates the idea of canonical iteration, demonstrating
   fast accumulation of tree content using a text buffer.
 \<close>
 
 ML \<open>
   datatype tree = Text of string | Elem of string * tree list;
 
   fun slow_content (Text txt) = txt
     | slow_content (Elem (name, ts)) =
         "<" ^ name ^ ">" ^
         implode (map slow_content ts) ^
         "</" ^ name ^ ">"
 
   fun add_content (Text txt) = Buffer.add txt
     | add_content (Elem (name, ts)) =
         Buffer.add ("<" ^ name ^ ">") #>
         fold add_content ts #>
         Buffer.add ("</" ^ name ^ ">");
 
   fun fast_content tree =
     Buffer.empty |> add_content tree |> Buffer.content;
 \<close>
 
 text \<open>
   The slowness of \<^ML>\<open>slow_content\<close> is due to the \<^ML>\<open>implode\<close> of the
   recursive results, because it copies previously produced strings again and
   again.
 
   The incremental \<^ML>\<open>add_content\<close> avoids this by operating on a buffer that
   is passed through in a linear fashion. Using \<^ML_text>\<open>#>\<close> and contraction
   over the actual buffer argument saves some additional boiler-plate. Of
   course, the two \<^ML>\<open>Buffer.add\<close> invocations with concatenated strings
   could have been split into smaller parts, but this would have obfuscated the
   source without making a big difference in performance. Here we have done
   some peephole-optimization for the sake of readability.
 
   Another benefit of \<^ML>\<open>add_content\<close> is its ``open'' form as a function on
   buffers that can be continued in further linear transformations, folding
   etc. Thus it is more compositional than the naive \<^ML>\<open>slow_content\<close>. As
   realistic example, compare the old-style
-  \<^ML>\<open>Term.maxidx_of_term: term -> int\<close> with the newer \<^ML>\<open>Term.maxidx_term: term -> int -> int\<close> in Isabelle/Pure.
+  \<^ML>\<open>Term.maxidx_of_term: term -> int\<close> with the newer
+  \<^ML>\<open>Term.maxidx_term: term -> int -> int\<close> in Isabelle/Pure.
 
   Note that \<^ML>\<open>fast_content\<close> above is only defined as example. In many
-  practical situations, it is customary to provide the incremental \<^ML>\<open>add_content\<close> only and leave the initialization and termination to the
+  practical situations, it is customary to provide the incremental
+  \<^ML>\<open>add_content\<close> only and leave the initialization and termination to the
   concrete application to the user.
 \<close>
 
 
 section \<open>Message output channels \label{sec:message-channels}\<close>
 
 text \<open>
   Isabelle provides output channels for different kinds of messages: regular
   output, high-volume tracing information, warnings, and errors.
 
   Depending on the user interface involved, these messages may appear in
   different text styles or colours. The standard output for batch sessions
   prefixes each line of warnings by \<^verbatim>\<open>###\<close> and errors by \<^verbatim>\<open>***\<close>, but leaves
   anything else unchanged. The message body may contain further markup and
   formatting, which is routinely used in the Prover IDE @{cite
   "isabelle-jedit"}.
 
   Messages are associated with the transaction context of the running Isar
   command. This enables the front-end to manage commands and resulting
   messages together. For example, after deleting a command from a given theory
   document version, the corresponding message output can be retracted from the
   display.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML writeln: "string -> unit"} \\
   @{define_ML tracing: "string -> unit"} \\
   @{define_ML warning: "string -> unit"} \\
   @{define_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>writeln\<close>~\<open>text\<close> outputs \<open>text\<close> as regular message. This is the
   primary message output operation of Isabelle and should be used by default.
 
   \<^descr> \<^ML>\<open>tracing\<close>~\<open>text\<close> outputs \<open>text\<close> as special tracing message, indicating
   potential high-volume output to the front-end (hundreds or thousands of
   messages issued by a single command). The idea is to allow the
   user-interface to downgrade the quality of message display to achieve higher
   throughput.
 
   Note that the user might have to take special actions to see tracing output,
   e.g.\ switch to a different output window. So this channel should not be
   used for regular output.
 
   \<^descr> \<^ML>\<open>warning\<close>~\<open>text\<close> outputs \<open>text\<close> as warning, which typically means some
   extra emphasis on the front-end side (color highlighting, icons, etc.).
 
   \<^descr> \<^ML>\<open>error\<close>~\<open>text\<close> raises exception \<^ML>\<open>ERROR\<close>~\<open>text\<close> and thus lets the
   Isar toplevel print \<open>text\<close> on the error channel, which typically means some
   extra emphasis on the front-end side (color highlighting, icons, etc.).
 
   This assumes that the exception is not handled before the command
   terminates. Handling exception \<^ML>\<open>ERROR\<close>~\<open>text\<close> is a perfectly legal
   alternative: it means that the error is absorbed without any message output.
 
   \begin{warn}
   The actual error channel is accessed via \<^ML>\<open>Output.error_message\<close>, but
   this is normally not used directly in user code.
   \end{warn}
 
 
   \begin{warn}
   Regular Isabelle/ML code should output messages exclusively by the official
-  channels. Using raw I/O on \<^emph>\<open>stdout\<close> or \<^emph>\<open>stderr\<close> instead (e.g.\ via \<^ML>\<open>TextIO.output\<close>) is apt to cause problems in the presence of parallel and
-  asynchronous processing of Isabelle theories. Such raw output might be
+  channels. Using raw I/O on \<^emph>\<open>stdout\<close> or \<^emph>\<open>stderr\<close> instead (e.g.\ via
+  \<^ML>\<open>TextIO.output\<close>) is apt to cause problems in the presence of parallel
+  and asynchronous processing of Isabelle theories. Such raw output might be
   displayed by the front-end in some system console log, with a low chance
   that the user will ever see it. Moreover, as a genuine side-effect on global
   process channels, there is no proper way to retract output when Isar command
   transactions are reset by the system.
   \end{warn}
 
   \begin{warn}
   The message channels should be used in a message-oriented manner. This means
   that multi-line output that logically belongs together is issued by a single
   invocation of \<^ML>\<open>writeln\<close> etc.\ with the functional concatenation of all
   message constituents.
   \end{warn}
 \<close>
 
 text %mlex \<open>
   The following example demonstrates a multi-line warning. Note that in some
   situations the user sees only the first line, so the most important point
   should be made first.
 \<close>
 
 ML_command \<open>
   warning (cat_lines
    ["Beware the Jabberwock, my son!",
     "The jaws that bite, the claws that catch!",
     "Beware the Jubjub Bird, and shun",
     "The frumious Bandersnatch!"]);
 \<close>
 
 text \<open>
   \<^medskip>
   An alternative is to make a paragraph of freely-floating words as follows.
 \<close>
 
 ML_command \<open>
   warning (Pretty.string_of (Pretty.para
     "Beware the Jabberwock, my son! \
     \The jaws that bite, the claws that catch! \
     \Beware the Jubjub Bird, and shun \
     \The frumious Bandersnatch!"))
 \<close>
 
 text \<open>
   This has advantages with variable window / popup sizes, but might make it
   harder to search for message content systematically, e.g.\ by other tools or
   by humans expecting the ``verse'' of a formal message in a fixed layout.
 \<close>
 
 
 section \<open>Exceptions \label{sec:exceptions}\<close>
 
 text \<open>
   The Standard ML semantics of strict functional evaluation together with
   exceptions is rather well defined, but some delicate points need to be
   observed to avoid that ML programs go wrong despite static type-checking.
   Exceptions in Isabelle/ML are subsequently categorized as follows.
 \<close>
 
 paragraph \<open>Regular user errors.\<close>
 text \<open>
   These are meant to provide informative feedback about malformed input etc.
 
   The \<^emph>\<open>error\<close> function raises the corresponding \<^ML>\<open>ERROR\<close> exception, with a
   plain text message as argument. \<^ML>\<open>ERROR\<close> exceptions can be handled
   internally, in order to be ignored, turned into other exceptions, or
   cascaded by appending messages. If the corresponding Isabelle/Isar command
   terminates with an \<^ML>\<open>ERROR\<close> exception state, the system will print the
   result on the error channel (see \secref{sec:message-channels}).
 
   It is considered bad style to refer to internal function names or values in
   ML source notation in user error messages. Do not use \<open>@{make_string}\<close> nor
   \<open>@{here}\<close>!
 
   Grammatical correctness of error messages can be improved by \<^emph>\<open>omitting\<close>
   final punctuation: messages are often concatenated or put into a larger
   context (e.g.\ augmented with source position). Note that punctuation after
   formal entities (types, terms, theorems) is particularly prone to user
   confusion.
 \<close>
 
 paragraph \<open>Program failures.\<close>
 text \<open>
   There is a handful of standard exceptions that indicate general failure
   situations, or failures of core operations on logical entities (types,
   terms, theorems, theories, see \chref{ch:logic}).
 
   These exceptions indicate a genuine breakdown of the program, so the main
   purpose is to determine quickly what has happened where. Traditionally, the
   (short) exception message would include the name of an ML function, although
   this is no longer necessary, because the ML runtime system attaches detailed
   source position stemming from the corresponding \<^ML_text>\<open>raise\<close> keyword.
 
   \<^medskip>
   User modules can always introduce their own custom exceptions locally, e.g.\
   to organize internal failures robustly without overlapping with existing
   exceptions. Exceptions that are exposed in module signatures require extra
   care, though, and should \<^emph>\<open>not\<close> be introduced by default. Surprise by users
   of a module can be often minimized by using plain user errors instead.
 \<close>
 
 paragraph \<open>Interrupts.\<close>
 text \<open>
   These indicate arbitrary system events: both the ML runtime system and the
   Isabelle/ML infrastructure signal various exceptional situations by raising
   the special \<^ML>\<open>Exn.Interrupt\<close> exception in user code.
 
   This is the one and only way that physical events can intrude an Isabelle/ML
   program. Such an interrupt can mean out-of-memory, stack overflow, timeout,
   internal signaling of threads, or a POSIX process signal. An Isabelle/ML
   program that intercepts interrupts becomes dependent on physical effects of
   the environment. Even worse, exception handling patterns that are too
   general by accident, e.g.\ by misspelled exception constructors, will cover
   interrupts unintentionally and thus render the program semantics
   ill-defined.
 
   Note that the Interrupt exception dates back to the original SML90 language
   definition. It was excluded from the SML97 version to avoid its malign
   impact on ML program semantics, but without providing a viable alternative.
   Isabelle/ML recovers physical interruptibility (which is an indispensable
   tool to implement managed evaluation of command transactions), but requires
   user code to be strictly transparent wrt.\ interrupts.
 
   \begin{warn}
   Isabelle/ML user code needs to terminate promptly on interruption, without
   guessing at its meaning to the system infrastructure. Temporary handling of
   interrupts for cleanup of global resources etc.\ needs to be followed
   immediately by re-raising of the original exception.
   \end{warn}
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
   @{define_ML can: "('a -> 'b) -> 'a -> bool"} \\
   @{define_ML_exception ERROR of string} \\
   @{define_ML_exception Fail of string} \\
   @{define_ML Exn.is_interrupt: "exn -> bool"} \\
   @{define_ML Exn.reraise: "exn -> 'a"} \\
   @{define_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
   \<^rail>\<open>
     (@@{ML_antiquotation try} | @@{ML_antiquotation can}) embedded
   \<close>
 
   \<^descr> \<^ML>\<open>try\<close>~\<open>f x\<close> makes the partiality of evaluating \<open>f x\<close> explicit via the
   option datatype. Interrupts are \<^emph>\<open>not\<close> handled here, i.e.\ this form serves
   as safe replacement for the \<^emph>\<open>unsafe\<close> version \<^ML_text>\<open>(SOME\<close>~\<open>f
   x\<close>~\<^ML_text>\<open>handle _ => NONE)\<close> that is occasionally seen in books about
   SML97, but not in Isabelle/ML.
 
   \<^descr> \<^ML>\<open>can\<close> is similar to \<^ML>\<open>try\<close> with more abstract result.
 
   \<^descr> \<^ML>\<open>ERROR\<close>~\<open>msg\<close> represents user errors; this exception is normally
   raised indirectly via the \<^ML>\<open>error\<close> function (see
   \secref{sec:message-channels}).
 
   \<^descr> \<^ML>\<open>Fail\<close>~\<open>msg\<close> represents general program failures.
 
   \<^descr> \<^ML>\<open>Exn.is_interrupt\<close> identifies interrupts robustly, without mentioning
   concrete exception constructors in user code. Handled interrupts need to be
   re-raised promptly!
 
   \<^descr> \<^ML>\<open>Exn.reraise\<close>~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit
   position information (if possible, depending on the ML platform).
 
   \<^descr> \<^ML>\<open>Runtime.exn_trace\<close>~\<^ML_text>\<open>(fn () =>\<close>~\<open>e\<close>\<^ML_text>\<open>)\<close> evaluates
   expression \<open>e\<close> while printing a full trace of its stack of nested exceptions
   (if possible, depending on the ML platform).
 
   Inserting \<^ML>\<open>Runtime.exn_trace\<close> into ML code temporarily is useful for
   debugging, but not suitable for production code.
 \<close>
 
 text %mlantiq \<open>
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "try"} & : & \<open>ML_antiquotation\<close> \\
   @{ML_antiquotation_def "can"} & : & \<open>ML_antiquotation\<close> \\
   @{ML_antiquotation_def "assert"} & : & \<open>ML_antiquotation\<close> \\
   @{ML_antiquotation_def "undefined"} & : & \<open>ML_antiquotation\<close> \\
   \end{matharray}
 
   \<^descr> \<open>@{try}\<close> and \<open>{can}\<close> are similar to the corresponding functions, but the
   argument is taken directly as ML expression: functional abstraction and
   application is done implicitly.
 
   \<^descr> \<open>@{assert}\<close> inlines a function \<^ML_type>\<open>bool -> unit\<close> that raises
   \<^ML>\<open>Fail\<close> if the argument is \<^ML>\<open>false\<close>. Due to inlining the source
   position of failed assertions is included in the error output.
 
   \<^descr> \<open>@{undefined}\<close> inlines \<^verbatim>\<open>raise\<close>~\<^ML>\<open>Match\<close>, i.e.\ the ML program
   behaves as in some function application of an undefined case.
 \<close>
 
 text %mlex \<open>
   We define a total version of division: any failures are swept under the
   carpet and mapped to a default value. Thus division-by-zero becomes 0, but
   there could be other exceptions like overflow that produce the same result
   (for unbounded integers this does not happen).
 \<close>
 
 ML \<open>
   fun div_total x y = \<^try>\<open>x div y\<close> |> the_default 0;
 
   \<^assert> (div_total 1 0 = 0);
 \<close>
 
 text \<open>
   The ML function \<^ML>\<open>undefined\<close> is defined in \<^file>\<open>~~/src/Pure/library.ML\<close>
   as follows:
 \<close>
 
 ML \<open>fun undefined _ = raise Match\<close>
 
 text \<open>
   \<^medskip>
   The following variant uses the antiquotation @{ML_antiquotation undefined}
   instead:
 \<close>
 
 ML \<open>fun undefined _ = \<^undefined>\<close>
 
 text \<open>
   \<^medskip>
   Here is the same, using control-symbol notation for the antiquotation, with
   special rendering of \<^verbatim>\<open>\<^undefined>\<close>:
 \<close>
 
 ML \<open>fun undefined _ = \<^undefined>\<close>
 
 text \<open>
   \<^medskip> Semantically, all forms are equivalent to a function definition
   without any clauses, but that is syntactically not allowed in ML.
 \<close>
 
 
 section \<open>Strings of symbols \label{sec:symbols}\<close>
 
 text \<open>
   A \<^emph>\<open>symbol\<close> constitutes the smallest textual unit in Isabelle/ML --- raw ML
   characters are normally not encountered at all. Isabelle strings consist of
   a sequence of symbols, represented as a packed string or an exploded list of
   strings. Each symbol is in itself a small string, which has either one of
   the following forms:
 
     \<^enum> a single ASCII character ``\<open>c\<close>'', for example ``\<^verbatim>\<open>a\<close>'',
 
     \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
 
     \<^enum> a regular symbol ``\<^verbatim>\<open>\<ident>\<close>'', for example ``\<^verbatim>\<open>\<alpha>\<close>'',
 
     \<^enum> a control symbol ``\<^verbatim>\<open>\<^ident>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
 
   The \<open>ident\<close> syntax for symbol names is \<open>letter (letter | digit)\<^sup>*\<close>, where
   \<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>. There are infinitely many regular
   symbols and control symbols, but a fixed collection of standard symbols is
   treated specifically. For example, ``\<^verbatim>\<open>\<alpha>\<close>'' is classified as a letter, which
   means it may occur within regular Isabelle identifiers.
 
   The character set underlying Isabelle symbols is 7-bit ASCII, but 8-bit
   character sequences are passed-through unchanged. Unicode/UCS data in UTF-8
   encoding is processed in a non-strict fashion, such that well-formed code
   sequences are recognized accordingly. Unicode provides its own collection of
   mathematical symbols, but within the core Isabelle/ML world there is no link
   to the standard collection of Isabelle regular symbols.
 
   \<^medskip>
   Output of Isabelle symbols depends on the print mode. For example, the
   standard {\LaTeX} setup of the Isabelle document preparation system would
   present ``\<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>, and ``\<^verbatim>\<open>\<^bold>\<alpha>\<close>'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering usually
   works by mapping a finite subset of Isabelle symbols to suitable Unicode
   characters.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type Symbol.symbol = string} \\
   @{define_ML Symbol.explode: "string -> Symbol.symbol list"} \\
   @{define_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   @{define_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
   @{define_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
   @{define_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
   \end{mldecls}
   \begin{mldecls}
   @{define_ML_type "Symbol.sym"} \\
   @{define_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Symbol.symbol\<close> represents individual Isabelle symbols.
 
   \<^descr> \<^ML>\<open>Symbol.explode\<close>~\<open>str\<close> produces a symbol list from the packed form.
   This function supersedes \<^ML>\<open>String.explode\<close> for virtually all purposes
   of manipulating text in Isabelle!\<^footnote>\<open>The runtime overhead for exploded strings
   is mainly that of the list structure: individual symbols that happen to be a
   singleton string do not require extra memory in Poly/ML.\<close>
 
-  \<^descr> \<^ML>\<open>Symbol.is_letter\<close>, \<^ML>\<open>Symbol.is_digit\<close>, \<^ML>\<open>Symbol.is_quasi\<close>, \<^ML>\<open>Symbol.is_blank\<close> classify standard symbols
+  \<^descr> \<^ML>\<open>Symbol.is_letter\<close>, \<^ML>\<open>Symbol.is_digit\<close>,
+  \<^ML>\<open>Symbol.is_quasi\<close>, \<^ML>\<open>Symbol.is_blank\<close> classify standard symbols
   according to fixed syntactic conventions of Isabelle, cf.\ @{cite
   "isabelle-isar-ref"}.
 
   \<^descr> Type \<^ML_type>\<open>Symbol.sym\<close> is a concrete datatype that represents the
-  different kinds of symbols explicitly, with constructors \<^ML>\<open>Symbol.Char\<close>, \<^ML>\<open>Symbol.UTF8\<close>, \<^ML>\<open>Symbol.Sym\<close>, \<^ML>\<open>Symbol.Control\<close>, \<^ML>\<open>Symbol.Malformed\<close>.
+  different kinds of symbols explicitly, with constructors
+  \<^ML>\<open>Symbol.Char\<close>, \<^ML>\<open>Symbol.UTF8\<close>, \<^ML>\<open>Symbol.Sym\<close>,
+  \<^ML>\<open>Symbol.Control\<close>, \<^ML>\<open>Symbol.Malformed\<close>.
 
   \<^descr> \<^ML>\<open>Symbol.decode\<close> converts the string representation of a symbol into
   the datatype version.
 \<close>
 
 paragraph \<open>Historical note.\<close>
 text \<open>
   In the original SML90 standard the primitive ML type \<^ML_type>\<open>char\<close> did not
   exists, and \<^ML_text>\<open>explode: string -> string list\<close> produced a list of
   singleton strings like \<^ML>\<open>raw_explode: string -> string list\<close> in
   Isabelle/ML today. When SML97 came out, Isabelle did not adopt its somewhat
   anachronistic 8-bit or 16-bit characters, but the idea of exploding a string
   into a list of small strings was extended to ``symbols'' as explained above.
   Thus Isabelle sources can refer to an infinite store of user-defined
   symbols, without having to worry about the multitude of Unicode encodings
   that have emerged over the years.
 \<close>
 
 
 section \<open>Basic data types\<close>
 
 text \<open>
   The basis library proposal of SML97 needs to be treated with caution. Many
   of its operations simply do not fit with important Isabelle/ML conventions
   (like ``canonical argument order'', see
   \secref{sec:canonical-argument-order}), others cause problems with the
-  parallel evaluation model of Isabelle/ML (such as \<^ML>\<open>TextIO.print\<close> or \<^ML>\<open>OS.Process.system\<close>).
+  parallel evaluation model of Isabelle/ML (such as \<^ML>\<open>TextIO.print\<close> or
+  \<^ML>\<open>OS.Process.system\<close>).
 
   Subsequently we give a brief overview of important operations on basic ML
   data types.
 \<close>
 
 
 subsection \<open>Characters\<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type char} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>char\<close> is \<^emph>\<open>not\<close> used. The smallest textual unit in Isabelle
   is represented as a ``symbol'' (see \secref{sec:symbols}).
 \<close>
 
 
 subsection \<open>Strings\<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type string} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>string\<close> represents immutable vectors of 8-bit characters.
   There are operations in SML to convert back and forth to actual byte
   vectors, which are seldom used.
 
   This historically important raw text representation is used for
   Isabelle-specific purposes with the following implicit substructures packed
   into the string content:
 
-    \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), with \<^ML>\<open>Symbol.explode\<close> as key operation;
+    \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), with
+    \<^ML>\<open>Symbol.explode\<close> as key operation;
   
     \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}), with
     \<^ML>\<open>YXML.parse_body\<close> as key operation.
 
   Note that Isabelle/ML string literals may refer Isabelle symbols like
   ``\<^verbatim>\<open>\<alpha>\<close>'' natively, \<^emph>\<open>without\<close> escaping the backslash. This is a consequence
   of Isabelle treating all source text as strings of symbols, instead of raw
   characters.
 \<close>
 
 text %mlex \<open>
   The subsequent example illustrates the difference of physical addressing of
   bytes versus logical addressing of symbols in Isabelle strings.
 \<close>
 
 ML_val \<open>
   val s = "\<A>";
 
   \<^assert> (length (Symbol.explode s) = 1);
   \<^assert> (size s = 4);
 \<close>
 
 text \<open>
   Note that in Unicode renderings of the symbol \<open>\<A>\<close>, variations of encodings
   like UTF-8 or UTF-16 pose delicate questions about the multi-byte
   representations of its codepoint, which is outside of the 16-bit address
   space of the original Unicode standard from the 1990-ies. In Isabelle/ML it
   is just ``\<^verbatim>\<open>\<A>\<close>'' literally, using plain ASCII characters beyond any
   doubts.
 \<close>
 
 
 subsection \<open>Integers\<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type int} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>int\<close> represents regular mathematical integers, which are
   \<^emph>\<open>unbounded\<close>. Overflow is treated properly, but should never happen in
   practice.\<^footnote>\<open>The size limit for integer bit patterns in memory is 64\,MB for
   32-bit Poly/ML, and much higher for 64-bit systems.\<close>
 
   Structure \<^ML_structure>\<open>IntInf\<close> of SML97 is obsolete and superseded by
   \<^ML_structure>\<open>Int\<close>. Structure \<^ML_structure>\<open>Integer\<close> in
   \<^file>\<open>~~/src/Pure/General/integer.ML\<close> provides some additional operations.
 \<close>
 
 
 subsection \<open>Rational numbers\<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type Rat.rat} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Rat.rat\<close> represents rational numbers, based on the
   unbounded integers of Poly/ML.
 
   Literal rationals may be written with special antiquotation syntax
   \<^verbatim>\<open>@\<close>\<open>int\<close>\<^verbatim>\<open>/\<close>\<open>nat\<close> or \<^verbatim>\<open>@\<close>\<open>int\<close> (without any white space). For example
   \<^verbatim>\<open>@~1/4\<close> or \<^verbatim>\<open>@10\<close>. The ML toplevel pretty printer uses the same format.
 
   Standard operations are provided via ad-hoc overloading of \<^verbatim>\<open>+\<close>, \<^verbatim>\<open>-\<close>, \<^verbatim>\<open>*\<close>,
   \<^verbatim>\<open>/\<close>, etc.
 \<close>
 
 
 subsection \<open>Time\<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type Time.time} \\
   @{define_ML seconds: "real -> Time.time"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>Time.time\<close> represents time abstractly according to the
   SML97 basis library definition. This is adequate for internal ML operations,
   but awkward in concrete time specifications.
 
   \<^descr> \<^ML>\<open>seconds\<close>~\<open>s\<close> turns the concrete scalar \<open>s\<close> (measured in seconds) into
   an abstract time value. Floating point numbers are easy to use as
   configuration options in the context (see \secref{sec:config-options}) or
   system options that are maintained externally.
 \<close>
 
 
 subsection \<open>Options\<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML Option.map: "('a -> 'b) -> 'a option -> 'b option"} \\
   @{define_ML is_some: "'a option -> bool"} \\
   @{define_ML is_none: "'a option -> bool"} \\
   @{define_ML the: "'a option -> 'a"} \\
   @{define_ML these: "'a list option -> 'a list"} \\
   @{define_ML the_list: "'a option -> 'a list"} \\
   @{define_ML the_default: "'a -> 'a option -> 'a"} \\
   \end{mldecls}
 \<close>
 
 text \<open>
   Apart from \<^ML>\<open>Option.map\<close> most other operations defined in structure
   \<^ML_structure>\<open>Option\<close> are alien to Isabelle/ML and never used. The
   operations shown above are defined in \<^file>\<open>~~/src/Pure/General/basics.ML\<close>.
 \<close>
 
 
 subsection \<open>Lists\<close>
 
 text \<open>
   Lists are ubiquitous in ML as simple and light-weight ``collections'' for
   many everyday programming tasks. Isabelle/ML provides important additions
   and improvements over operations that are predefined in the SML97 library.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML cons: "'a -> 'a list -> 'a list"} \\
   @{define_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
   @{define_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
   @{define_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
   @{define_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>cons\<close>~\<open>x xs\<close> evaluates to \<open>x :: xs\<close>.
 
   Tupled infix operators are a historical accident in Standard ML. The curried
   \<^ML>\<open>cons\<close> amends this, but it should be only used when partial application
   is required.
 
   \<^descr> \<^ML>\<open>member\<close>, \<^ML>\<open>insert\<close>, \<^ML>\<open>remove\<close>, \<^ML>\<open>update\<close> treat lists as a
   set-like container that maintains the order of elements. See
   \<^file>\<open>~~/src/Pure/library.ML\<close> for the full specifications (written in ML).
   There are some further derived operations like \<^ML>\<open>union\<close> or \<^ML>\<open>inter\<close>.
 
   Note that \<^ML>\<open>insert\<close> is conservative about elements that are already a
   \<^ML>\<open>member\<close> of the list, while \<^ML>\<open>update\<close> ensures that the latest entry
   is always put in front. The latter discipline is often more appropriate in
   declarations of context data (\secref{sec:context-data}) that are issued by
   the user in Isar source: later declarations take precedence over earlier
   ones. \<close>
 
 text %mlex \<open>
   Using canonical \<^ML>\<open>fold\<close> together with \<^ML>\<open>cons\<close> (or similar standard
   operations) alternates the orientation of data. The is quite natural and
   should not be altered forcible by inserting extra applications of \<^ML>\<open>rev\<close>.
   The alternative \<^ML>\<open>fold_rev\<close> can be used in the few situations, where
   alternation should be prevented.
 \<close>
 
 ML_val \<open>
   val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
 
   val list1 = fold cons items [];
   \<^assert> (list1 = rev items);
 
   val list2 = fold_rev cons items [];
   \<^assert> (list2 = items);
 \<close>
 
 text \<open>
   The subsequent example demonstrates how to \<^emph>\<open>merge\<close> two lists in a natural
   way.
 \<close>
 
 ML_val \<open>
   fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs;
 \<close>
 
 text \<open>
   Here the first list is treated conservatively: only the new elements from
-  the second list are inserted. The inside-out order of insertion via \<^ML>\<open>fold_rev\<close> attempts to preserve the order of elements in the result.
+  the second list are inserted. The inside-out order of insertion via
+  \<^ML>\<open>fold_rev\<close> attempts to preserve the order of elements in the result.
 
   This way of merging lists is typical for context data
   (\secref{sec:context-data}). See also \<^ML>\<open>merge\<close> as defined in
   \<^file>\<open>~~/src/Pure/library.ML\<close>.
 \<close>
 
 
 subsection \<open>Association lists\<close>
 
 text \<open>
   The operations for association lists interpret a concrete list of pairs as a
   finite function from keys to values. Redundant representations with multiple
   occurrences of the same key are implicitly normalized: lookup and update
   only take the first occurrence into account.
 \<close>
 
 text \<open>
   \begin{mldecls}
   @{define_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\
   @{define_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\
   @{define_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>AList.lookup\<close>, \<^ML>\<open>AList.defined\<close>, \<^ML>\<open>AList.update\<close> implement the
   main ``framework operations'' for mappings in Isabelle/ML, following
   standard conventions for their names and types.
 
   Note that a function called \<^verbatim>\<open>lookup\<close> is obliged to express its partiality
   via an explicit option element. There is no choice to raise an exception,
   without changing the name to something like \<open>the_element\<close> or \<open>get\<close>.
 
   The \<open>defined\<close> operation is essentially a contraction of \<^ML>\<open>is_some\<close> and
   \<^verbatim>\<open>lookup\<close>, but this is sufficiently frequent to justify its independent
   existence. This also gives the implementation some opportunity for peep-hole
   optimization.
 
 
   Association lists are adequate as simple implementation of finite mappings
   in many practical situations. A more advanced table structure is defined in
   \<^file>\<open>~~/src/Pure/General/table.ML\<close>; that version scales easily to thousands or
   millions of elements.
 \<close>
 
 
 subsection \<open>Unsynchronized references\<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type 'a "Unsynchronized.ref"} \\
   @{define_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
   @{define_ML "!": "'a Unsynchronized.ref -> 'a"} \\
   @{define_ML_infix ":=" : "'a Unsynchronized.ref * 'a -> unit"} \\
   \end{mldecls}
 \<close>
 
 text \<open>
   Due to ubiquitous parallelism in Isabelle/ML (see also
   \secref{sec:multi-threading}), the mutable reference cells of Standard ML
   are notorious for causing problems. In a highly parallel system, both
   correctness \<^emph>\<open>and\<close> performance are easily degraded when using mutable data.
 
   The unwieldy name of \<^ML>\<open>Unsynchronized.ref\<close> for the constructor for
   references in Isabelle/ML emphasizes the inconveniences caused by
   mutability. Existing operations \<^ML>\<open>!\<close> and \<^ML_infix>\<open>:=\<close> are unchanged,
   but should be used with special precautions, say in a strictly local
   situation that is guaranteed to be restricted to sequential evaluation ---
   now and in the future.
 
   \begin{warn}
   Never \<^ML_text>\<open>open Unsynchronized\<close>, not even in a local scope!
   Pretending that mutable state is no problem is a very bad idea.
   \end{warn}
 \<close>
 
 
 section \<open>Thread-safe programming \label{sec:multi-threading}\<close>
 
 text \<open>
   Multi-threaded execution has become an everyday reality in Isabelle since
   Poly/ML 5.2.1 and Isabelle2008. Isabelle/ML provides implicit and explicit
   parallelism by default, and there is no way for user-space tools to ``opt
   out''. ML programs that are purely functional, output messages only via the
   official channels (\secref{sec:message-channels}), and do not intercept
   interrupts (\secref{sec:exceptions}) can participate in the multi-threaded
   environment immediately without further ado.
 
   More ambitious tools with more fine-grained interaction with the environment
   need to observe the principles explained below.
 \<close>
 
 
 subsection \<open>Multi-threading with shared memory\<close>
 
 text \<open>
   Multiple threads help to organize advanced operations of the system, such as
   real-time conditions on command transactions, sub-components with explicit
   communication, general asynchronous interaction etc. Moreover, parallel
   evaluation is a prerequisite to make adequate use of the CPU resources that
   are available on multi-core systems.\<^footnote>\<open>Multi-core computing does not mean
   that there are ``spare cycles'' to be wasted. It means that the continued
   exponential speedup of CPU performance due to ``Moore's Law'' follows
   different rules: clock frequency has reached its peak around 2005, and
   applications need to be parallelized in order to avoid a perceived loss of
   performance. See also @{cite "Sutter:2005"}.\<close>
 
   Isabelle/Isar exploits the inherent structure of theories and proofs to
   support \<^emph>\<open>implicit parallelism\<close> to a large extent. LCF-style theorem proving
   provides almost ideal conditions for that, see also @{cite "Wenzel:2009"}.
   This means, significant parts of theory and proof checking is parallelized
   by default. In Isabelle2013, a maximum speedup-factor of 3.5 on 4 cores and
   6.5 on 8 cores can be expected @{cite "Wenzel:2013:ITP"}.
 
   \<^medskip>
   ML threads lack the memory protection of separate processes, and operate
   concurrently on shared heap memory. This has the advantage that results of
   independent computations are directly available to other threads: abstract
   values can be passed without copying or awkward serialization that is
   typically required for separate processes.
 
   To make shared-memory multi-threading work robustly and efficiently, some
   programming guidelines need to be observed. While the ML system is
   responsible to maintain basic integrity of the representation of ML values
   in memory, the application programmer needs to ensure that multi-threaded
   execution does not break the intended semantics.
 
   \begin{warn}
   To participate in implicit parallelism, tools need to be thread-safe. A
   single ill-behaved tool can affect the stability and performance of the
   whole system.
   \end{warn}
 
   Apart from observing the principles of thread-safeness passively, advanced
   tools may also exploit parallelism actively, e.g.\ by using library
   functions for parallel list operations (\secref{sec:parlist}).
 
   \begin{warn}
   Parallel computing resources are managed centrally by the Isabelle/ML
   infrastructure. User programs should not fork their own ML threads to
   perform heavy computations.
   \end{warn}
 \<close>
 
 
 subsection \<open>Critical shared resources\<close>
 
 text \<open>
   Thread-safeness is mainly concerned about concurrent read/write access to
   shared resources, which are outside the purely functional world of ML. This
   covers the following in particular.
 
     \<^item> Global references (or arrays), i.e.\ mutable memory cells that persist
     over several invocations of associated operations.\<^footnote>\<open>This is independent of
     the visibility of such mutable values in the toplevel scope.\<close>
 
     \<^item> Global state of the running Isabelle/ML process, i.e.\ raw I/O channels,
     environment variables, current working directory.
 
     \<^item> Writable resources in the file-system that are shared among different
     threads or external processes.
 
   Isabelle/ML provides various mechanisms to avoid critical shared resources
   in most situations. As last resort there are some mechanisms for explicit
   synchronization. The following guidelines help to make Isabelle/ML programs
   work smoothly in a concurrent environment.
 
   \<^item> Avoid global references altogether. Isabelle/Isar maintains a uniform
   context that incorporates arbitrary data declared by user programs
   (\secref{sec:context-data}). This context is passed as plain value and user
   tools can get/map their own data in a purely functional manner.
   Configuration options within the context (\secref{sec:config-options})
   provide simple drop-in replacements for historic reference variables.
 
   \<^item> Keep components with local state information re-entrant. Instead of poking
   initial values into (private) global references, a new state record can be
   created on each invocation, and passed through any auxiliary functions of
   the component. The state record contain mutable references in special
   situations, without requiring any synchronization, as long as each
   invocation gets its own copy and the tool itself is single-threaded.
 
   \<^item> Avoid raw output on \<open>stdout\<close> or \<open>stderr\<close>. The Poly/ML library is
   thread-safe for each individual output operation, but the ordering of
   parallel invocations is arbitrary. This means raw output will appear on some
   system console with unpredictable interleaving of atomic chunks.
 
   Note that this does not affect regular message output channels
   (\secref{sec:message-channels}). An official message id is associated with
   the command transaction from where it originates, independently of other
   transactions. This means each running Isar command has effectively its own
   set of message channels, and interleaving can only happen when commands use
   parallelism internally (and only at message boundaries).
 
   \<^item> Treat environment variables and the current working directory of the
   running process as read-only.
 
   \<^item> Restrict writing to the file-system to unique temporary files. Isabelle
   already provides a temporary directory that is unique for the running
   process, and there is a centralized source of unique serial numbers in
   Isabelle/ML. Thus temporary files that are passed to to some external
   process will be always disjoint, and thus thread-safe.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML File.tmp_path: "Path.T -> Path.T"} \\
   @{define_ML serial_string: "unit -> string"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>File.tmp_path\<close>~\<open>path\<close> relocates the base component of \<open>path\<close> into the
   unique temporary directory of the running Isabelle/ML process.
 
   \<^descr> \<^ML>\<open>serial_string\<close>~\<open>()\<close> creates a new serial number that is unique over
   the runtime of the Isabelle/ML process.
 \<close>
 
 text %mlex \<open>
   The following example shows how to create unique temporary file names.
 \<close>
 
 ML_val \<open>
   val tmp1 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
   val tmp2 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
   \<^assert> (tmp1 <> tmp2);
 \<close>
 
 
 subsection \<open>Explicit synchronization\<close>
 
 text \<open>
   Isabelle/ML provides explicit synchronization for mutable variables over
   immutable data, which may be updated atomically and exclusively. This
   addresses the rare situations where mutable shared resources are really
   required. Synchronization in Isabelle/ML is based on primitives of Poly/ML,
   which have been adapted to the specific assumptions of the concurrent
   Isabelle environment. User code should not break this abstraction, but stay
   within the confines of concurrent Isabelle/ML.
 
   A \<^emph>\<open>synchronized variable\<close> is an explicit state component associated with
   mechanisms for locking and signaling. There are operations to await a
   condition, change the state, and signal the change to all other waiting
   threads. Synchronized access to the state variable is \<^emph>\<open>not\<close> re-entrant:
   direct or indirect nesting within the same thread will cause a deadlock!
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type 'a "Synchronized.var"} \\
   @{define_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\
   @{define_ML Synchronized.guarded_access: "'a Synchronized.var ->
   ('a -> ('b * 'a) option) -> 'b"} \\
   \end{mldecls}
 
     \<^descr> Type \<^ML_type>\<open>'a Synchronized.var\<close> represents synchronized variables
     with state of type \<^ML_type>\<open>'a\<close>.
 
     \<^descr> \<^ML>\<open>Synchronized.var\<close>~\<open>name x\<close> creates a synchronized variable that is
     initialized with value \<open>x\<close>. The \<open>name\<close> is used for tracing.
 
     \<^descr> \<^ML>\<open>Synchronized.guarded_access\<close>~\<open>var f\<close> lets the function \<open>f\<close> operate
     within a critical section on the state \<open>x\<close> as follows: if \<open>f x\<close> produces
     \<^ML>\<open>NONE\<close>, it continues to wait on the internal condition variable,
     expecting that some other thread will eventually change the content in a
     suitable manner; if \<open>f x\<close> produces \<^ML>\<open>SOME\<close>~\<open>(y, x')\<close> it is satisfied and
     assigns the new state value \<open>x'\<close>, broadcasts a signal to all waiting threads
     on the associated condition variable, and returns the result \<open>y\<close>.
 
   There are some further variants of the \<^ML>\<open>Synchronized.guarded_access\<close>
   combinator, see \<^file>\<open>~~/src/Pure/Concurrent/synchronized.ML\<close> for details.
 \<close>
 
 text %mlex \<open>
   The following example implements a counter that produces positive integers
   that are unique over the runtime of the Isabelle process:
 \<close>
 
 ML_val \<open>
   local
     val counter = Synchronized.var "counter" 0;
   in
     fun next () =
       Synchronized.guarded_access counter
         (fn i =>
           let val j = i + 1
           in SOME (j, j) end);
   end;
 
   val a = next ();
   val b = next ();
   \<^assert> (a <> b);
 \<close>
 
 text \<open>
   \<^medskip>
   See \<^file>\<open>~~/src/Pure/Concurrent/mailbox.ML\<close> how to implement a mailbox as
   synchronized variable over a purely functional list.
 \<close>
 
 
 section \<open>Managed evaluation\<close>
 
 text \<open>
   Execution of Standard ML follows the model of strict functional evaluation
   with optional exceptions. Evaluation happens whenever some function is
   applied to (sufficiently many) arguments. The result is either an explicit
   value or an implicit exception.
 
   \<^emph>\<open>Managed evaluation\<close> in Isabelle/ML organizes expressions and results to
   control certain physical side-conditions, to say more specifically when and
   how evaluation happens. For example, the Isabelle/ML library supports lazy
   evaluation with memoing, parallel evaluation via futures, asynchronous
   evaluation via promises, evaluation with time limit etc.
 
   \<^medskip>
   An \<^emph>\<open>unevaluated expression\<close> is represented either as unit abstraction
   \<^verbatim>\<open>fn () => a\<close> of type \<^verbatim>\<open>unit -> 'a\<close> or as regular function \<^verbatim>\<open>fn a => b\<close> of
   type \<^verbatim>\<open>'a -> 'b\<close>. Both forms occur routinely, and special care is required
   to tell them apart --- the static type-system of SML is only of limited help
   here.
 
   The first form is more intuitive: some combinator \<^verbatim>\<open>(unit -> 'a) -> 'a\<close>
   applies the given function to \<^verbatim>\<open>()\<close> to initiate the postponed evaluation
   process. The second form is more flexible: some combinator
   \<^verbatim>\<open>('a -> 'b) -> 'a -> 'b\<close> acts like a modified form of function application;
   several such combinators may be cascaded to modify a given function, before
   it is ultimately applied to some argument.
 
   \<^medskip>
   \<^emph>\<open>Reified results\<close> make the disjoint sum of regular values versions
   exceptional situations explicit as ML datatype: \<open>'a result = Res of 'a | Exn
   of exn\<close>. This is typically used for administrative purposes, to store the
   overall outcome of an evaluation process.
 
   \<^emph>\<open>Parallel exceptions\<close> aggregate reified results, such that multiple
   exceptions are digested as a collection in canonical form that identifies
   exceptions according to their original occurrence. This is particular
   important for parallel evaluation via futures \secref{sec:futures}, which
   are organized as acyclic graph of evaluations that depend on other
   evaluations: exceptions stemming from shared sub-graphs are exposed exactly
   once and in the order of their original occurrence (e.g.\ when printed at
   the toplevel). Interrupt counts as neutral element here: it is treated as
   minimal information about some canceled evaluation process, and is absorbed
   by the presence of regular program exceptions.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type 'a "Exn.result"} \\
   @{define_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
   @{define_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
   @{define_ML Exn.release: "'a Exn.result -> 'a"} \\
   @{define_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\
   @{define_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>'a Exn.result\<close> represents the disjoint sum of ML results
   explicitly, with constructor \<^ML>\<open>Exn.Res\<close> for regular values and \<^ML>\<open>Exn.Exn\<close> for exceptions.
 
   \<^descr> \<^ML>\<open>Exn.capture\<close>~\<open>f x\<close> manages the evaluation of \<open>f x\<close> such that
   exceptions are made explicit as \<^ML>\<open>Exn.Exn\<close>. Note that this includes
   physical interrupts (see also \secref{sec:exceptions}), so the same
   precautions apply to user code: interrupts must not be absorbed
   accidentally!
 
   \<^descr> \<^ML>\<open>Exn.interruptible_capture\<close> is similar to \<^ML>\<open>Exn.capture\<close>, but
   interrupts are immediately re-raised as required for user code.
 
   \<^descr> \<^ML>\<open>Exn.release\<close>~\<open>result\<close> releases the original runtime result, exposing
   its regular value or raising the reified exception.
 
   \<^descr> \<^ML>\<open>Par_Exn.release_all\<close>~\<open>results\<close> combines results that were produced
   independently (e.g.\ by parallel evaluation). If all results are regular
   values, that list is returned. Otherwise, the collection of all exceptions
   is raised, wrapped-up as collective parallel exception. Note that the latter
   prevents access to individual exceptions by conventional \<^verbatim>\<open>handle\<close> of ML.
 
   \<^descr> \<^ML>\<open>Par_Exn.release_first\<close> is similar to \<^ML>\<open>Par_Exn.release_all\<close>, but
   only the first (meaningful) exception that has occurred in the original
   evaluation process is raised again, the others are ignored. That single
   exception may get handled by conventional means in ML.
 \<close>
 
 
 subsection \<open>Parallel skeletons \label{sec:parlist}\<close>
 
 text \<open>
   Algorithmic skeletons are combinators that operate on lists in parallel, in
   the manner of well-known \<open>map\<close>, \<open>exists\<close>, \<open>forall\<close> etc. Management of
   futures (\secref{sec:futures}) and their results as reified exceptions is
   wrapped up into simple programming interfaces that resemble the sequential
   versions.
 
   What remains is the application-specific problem to present expressions with
   suitable \<^emph>\<open>granularity\<close>: each list element corresponds to one evaluation
   task. If the granularity is too coarse, the available CPUs are not
   saturated. If it is too fine-grained, CPU cycles are wasted due to the
   overhead of organizing parallel processing. In the worst case, parallel
   performance will be less than the sequential counterpart!
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML Par_List.map: "('a -> 'b) -> 'a list -> 'b list"} \\
   @{define_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Par_List.map\<close>~\<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> is like \<^ML>\<open>map\<close>~\<open>f [x\<^sub>1, \<dots>,
   x\<^sub>n]\<close>, but the evaluation of \<open>f x\<^sub>i\<close> for \<open>i = 1, \<dots>, n\<close> is performed in
   parallel.
 
   An exception in any \<open>f x\<^sub>i\<close> cancels the overall evaluation process. The
   final result is produced via \<^ML>\<open>Par_Exn.release_first\<close> as explained above,
   which means the first program exception that happened to occur in the
   parallel evaluation is propagated, and all other failures are ignored.
 
   \<^descr> \<^ML>\<open>Par_List.get_some\<close>~\<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> produces some \<open>f x\<^sub>i\<close> that is of
   the form \<open>SOME y\<^sub>i\<close>, if that exists, otherwise \<open>NONE\<close>. Thus it is similar to
   \<^ML>\<open>Library.get_first\<close>, but subject to a non-deterministic parallel choice
   process. The first successful result cancels the overall evaluation process;
   other exceptions are propagated as for \<^ML>\<open>Par_List.map\<close>.
 
   This generic parallel choice combinator is the basis for derived forms, such
   as \<^ML>\<open>Par_List.find_some\<close>, \<^ML>\<open>Par_List.exists\<close>, \<^ML>\<open>Par_List.forall\<close>.
 \<close>
 
 text %mlex \<open>
   Subsequently, the Ackermann function is evaluated in parallel for some
   ranges of arguments.
 \<close>
 
 ML_val \<open>
   fun ackermann 0 n = n + 1
     | ackermann m 0 = ackermann (m - 1) 1
     | ackermann m n = ackermann (m - 1) (ackermann m (n - 1));
 
   Par_List.map (ackermann 2) (500 upto 1000);
   Par_List.map (ackermann 3) (5 upto 10);
 \<close>
 
 
 subsection \<open>Lazy evaluation\<close>
 
 text \<open>
   Classic lazy evaluation works via the \<open>lazy\<close>~/ \<open>force\<close> pair of operations:
   \<open>lazy\<close> to wrap an unevaluated expression, and \<open>force\<close> to evaluate it once
   and store its result persistently. Later invocations of \<open>force\<close> retrieve the
   stored result without another evaluation. Isabelle/ML refines this idea to
   accommodate the aspects of multi-threading, synchronous program exceptions
   and asynchronous interrupts.
 
   The first thread that invokes \<open>force\<close> on an unfinished lazy value changes
   its state into a \<^emph>\<open>promise\<close> of the eventual result and starts evaluating it.
   Any other threads that \<open>force\<close> the same lazy value in the meantime need to
   wait for it to finish, by producing a regular result or program exception.
   If the evaluation attempt is interrupted, this event is propagated to all
   waiting threads and the lazy value is reset to its original state.
 
   This means a lazy value is completely evaluated at most once, in a
   thread-safe manner. There might be multiple interrupted evaluation attempts,
   and multiple receivers of intermediate interrupt events. Interrupts are
   \<^emph>\<open>not\<close> made persistent: later evaluation attempts start again from the
   original expression.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type 'a "lazy"} \\
   @{define_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\
   @{define_ML Lazy.value: "'a -> 'a lazy"} \\
   @{define_ML Lazy.force: "'a lazy -> 'a"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>'a lazy\<close> represents lazy values over type \<^verbatim>\<open>'a\<close>.
 
   \<^descr> \<^ML>\<open>Lazy.lazy\<close>~\<open>(fn () => e)\<close> wraps the unevaluated expression \<open>e\<close> as
   unfinished lazy value.
 
   \<^descr> \<^ML>\<open>Lazy.value\<close>~\<open>a\<close> wraps the value \<open>a\<close> as finished lazy value. When
   forced, it returns \<open>a\<close> without any further evaluation.
 
   There is very low overhead for this proforma wrapping of strict values as
   lazy values.
 
   \<^descr> \<^ML>\<open>Lazy.force\<close>~\<open>x\<close> produces the result of the lazy value in a
   thread-safe manner as explained above. Thus it may cause the current thread
   to wait on a pending evaluation attempt by another thread.
 \<close>
 
 
 subsection \<open>Futures \label{sec:futures}\<close>
 
 text \<open>
   Futures help to organize parallel execution in a value-oriented manner, with
   \<open>fork\<close>~/ \<open>join\<close> as the main pair of operations, and some further variants;
   see also @{cite "Wenzel:2009" and "Wenzel:2013:ITP"}. Unlike lazy values,
   futures are evaluated strictly and spontaneously on separate worker threads.
   Futures may be canceled, which leads to interrupts on running evaluation
   attempts, and forces structurally related futures to fail for all time;
   already finished futures remain unchanged. Exceptions between related
   futures are propagated as well, and turned into parallel exceptions (see
   above).
 
   Technically, a future is a single-assignment variable together with a
   \<^emph>\<open>task\<close> that serves administrative purposes, notably within the \<^emph>\<open>task
   queue\<close> where new futures are registered for eventual evaluation and the
   worker threads retrieve their work.
 
   The pool of worker threads is limited, in correlation with the number of
   physical cores on the machine. Note that allocation of runtime resources may
   be distorted either if workers yield CPU time (e.g.\ via system sleep or
   wait operations), or if non-worker threads contend for significant runtime
   resources independently. There is a limited number of replacement worker
   threads that get activated in certain explicit wait conditions, after a
   timeout.
 
   \<^medskip>
   Each future task belongs to some \<^emph>\<open>task group\<close>, which represents the
   hierarchic structure of related tasks, together with the exception status a
   that point. By default, the task group of a newly created future is a new
   sub-group of the presently running one, but it is also possible to indicate
   different group layouts under program control.
 
   Cancellation of futures actually refers to the corresponding task group and
   all its sub-groups. Thus interrupts are propagated down the group hierarchy.
   Regular program exceptions are treated likewise: failure of the evaluation
   of some future task affects its own group and all sub-groups. Given a
   particular task group, its \<^emph>\<open>group status\<close> cumulates all relevant exceptions
   according to its position within the group hierarchy. Interrupted tasks that
   lack regular result information, will pick up parallel exceptions from the
   cumulative group status.
 
   \<^medskip>
   A \<^emph>\<open>passive future\<close> or \<^emph>\<open>promise\<close> is a future with slightly different
   evaluation policies: there is only a single-assignment variable and some
   expression to evaluate for the \<^emph>\<open>failed\<close> case (e.g.\ to clean up resources
   when canceled). A regular result is produced by external means, using a
   separate \<^emph>\<open>fulfill\<close> operation.
 
   Promises are managed in the same task queue, so regular futures may depend
   on them. This allows a form of reactive programming, where some promises are
   used as minimal elements (or guards) within the future dependency graph:
   when these promises are fulfilled the evaluation of subsequent futures
   starts spontaneously, according to their own inter-dependencies.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type 'a "future"} \\
   @{define_ML Future.fork: "(unit -> 'a) -> 'a future"} \\
   @{define_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\
   @{define_ML Future.join: "'a future -> 'a"} \\
   @{define_ML Future.joins: "'a future list -> 'a list"} \\
   @{define_ML Future.value: "'a -> 'a future"} \\
   @{define_ML Future.map: "('a -> 'b) -> 'a future -> 'b future"} \\
   @{define_ML Future.cancel: "'a future -> unit"} \\
   @{define_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex]
   @{define_ML Future.promise: "(unit -> unit) -> 'a future"} \\
   @{define_ML Future.fulfill: "'a future -> 'a -> unit"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>'a future\<close> represents future values over type \<^verbatim>\<open>'a\<close>.
 
   \<^descr> \<^ML>\<open>Future.fork\<close>~\<open>(fn () => e)\<close> registers the unevaluated expression \<open>e\<close>
   as unfinished future value, to be evaluated eventually on the parallel
   worker-thread farm. This is a shorthand for \<^ML>\<open>Future.forks\<close> below, with
   default parameters and a single expression.
 
   \<^descr> \<^ML>\<open>Future.forks\<close>~\<open>params exprs\<close> is the general interface to fork several
   futures simultaneously. The \<open>params\<close> consist of the following fields:
 
     \<^item> \<open>name : string\<close> (default \<^ML>\<open>""\<close>) specifies a common name for the
     tasks of the forked futures, which serves diagnostic purposes.
 
     \<^item> \<open>group : Future.group option\<close> (default \<^ML>\<open>NONE\<close>) specifies an optional
     task group for the forked futures. \<^ML>\<open>NONE\<close> means that a new sub-group
     of the current worker-thread task context is created. If this is not a
     worker thread, the group will be a new root in the group hierarchy.
 
     \<^item> \<open>deps : Future.task list\<close> (default \<^ML>\<open>[]\<close>) specifies dependencies on
     other future tasks, i.e.\ the adjacency relation in the global task queue.
     Dependencies on already finished tasks are ignored.
 
     \<^item> \<open>pri : int\<close> (default \<^ML>\<open>0\<close>) specifies a priority within the task
     queue.
 
-    Typically there is only little deviation from the default priority \<^ML>\<open>0\<close>. As a rule of thumb, \<^ML>\<open>~1\<close> means ``low priority" and \<^ML>\<open>1\<close> means
-    ``high priority''.
+    Typically there is only little deviation from the default priority
+    \<^ML>\<open>0\<close>. As a rule of thumb, \<^ML>\<open>~1\<close> means ``low priority" and
+    \<^ML>\<open>1\<close> means ``high priority''.
 
     Note that the task priority only affects the position in the queue, not
     the thread priority. When a worker thread picks up a task for processing,
     it runs with the normal thread priority to the end (or until canceled).
     Higher priority tasks that are queued later need to wait until this (or
     another) worker thread becomes free again.
 
     \<^item> \<open>interrupts : bool\<close> (default \<^ML>\<open>true\<close>) tells whether the worker thread
     that processes the corresponding task is initially put into interruptible
     state. This state may change again while running, by modifying the thread
     attributes.
 
     With interrupts disabled, a running future task cannot be canceled. It is
     the responsibility of the programmer that this special state is retained
     only briefly.
 
   \<^descr> \<^ML>\<open>Future.join\<close>~\<open>x\<close> retrieves the value of an already finished future,
   which may lead to an exception, according to the result of its previous
   evaluation.
 
   For an unfinished future there are several cases depending on the role of
   the current thread and the status of the future. A non-worker thread waits
   passively until the future is eventually evaluated. A worker thread
   temporarily changes its task context and takes over the responsibility to
   evaluate the future expression on the spot. The latter is done in a
   thread-safe manner: other threads that intend to join the same future need
   to wait until the ongoing evaluation is finished.
 
   Note that excessive use of dynamic dependencies of futures by adhoc joining
   may lead to bad utilization of CPU cores, due to threads waiting on other
   threads to finish required futures. The future task farm has a limited
   amount of replacement threads that continue working on unrelated tasks after
   some timeout.
 
   Whenever possible, static dependencies of futures should be specified
   explicitly when forked (see \<open>deps\<close> above). Thus the evaluation can work from
   the bottom up, without join conflicts and wait states.
 
   \<^descr> \<^ML>\<open>Future.joins\<close>~\<open>xs\<close> joins the given list of futures simultaneously,
   which is more efficient than \<^ML>\<open>map Future.join\<close>~\<open>xs\<close>.
 
   Based on the dependency graph of tasks, the current thread takes over the
   responsibility to evaluate future expressions that are required for the main
   result, working from the bottom up. Waiting on future results that are
   presently evaluated on other threads only happens as last resort, when no
   other unfinished futures are left over.
 
   \<^descr> \<^ML>\<open>Future.value\<close>~\<open>a\<close> wraps the value \<open>a\<close> as finished future value,
   bypassing the worker-thread farm. When joined, it returns \<open>a\<close> without any
   further evaluation.
 
   There is very low overhead for this proforma wrapping of strict values as
   futures.
 
-  \<^descr> \<^ML>\<open>Future.map\<close>~\<open>f x\<close> is a fast-path implementation of \<^ML>\<open>Future.fork\<close>~\<open>(fn () => f (\<close>\<^ML>\<open>Future.join\<close>~\<open>x))\<close>, which avoids the full
-  overhead of the task queue and worker-thread farm as far as possible. The
-  function \<open>f\<close> is supposed to be some trivial post-processing or projection of
-  the future result.
+  \<^descr> \<^ML>\<open>Future.map\<close>~\<open>f x\<close> is a fast-path implementation of
+  \<^ML>\<open>Future.fork\<close>~\<open>(fn () => f (\<close>\<^ML>\<open>Future.join\<close>~\<open>x))\<close>, which avoids
+  the full overhead of the task queue and worker-thread farm as far as
+  possible. The function \<open>f\<close> is supposed to be some trivial post-processing or
+  projection of the future result.
 
   \<^descr> \<^ML>\<open>Future.cancel\<close>~\<open>x\<close> cancels the task group of the given future, using
   \<^ML>\<open>Future.cancel_group\<close> below.
 
   \<^descr> \<^ML>\<open>Future.cancel_group\<close>~\<open>group\<close> cancels all tasks of the given task
   group for all time. Threads that are presently processing a task of the
   given group are interrupted: it may take some time until they are actually
   terminated. Tasks that are queued but not yet processed are dequeued and
   forced into interrupted state. Since the task group is itself invalidated,
   any further attempt to fork a future that belongs to it will yield a
   canceled result as well.
 
   \<^descr> \<^ML>\<open>Future.promise\<close>~\<open>abort\<close> registers a passive future with the given
   \<open>abort\<close> operation: it is invoked when the future task group is canceled.
 
   \<^descr> \<^ML>\<open>Future.fulfill\<close>~\<open>x a\<close> finishes the passive future \<open>x\<close> by the given
   value \<open>a\<close>. If the promise has already been canceled, the attempt to fulfill
   it causes an exception.
 \<close>
 
 end
diff --git a/src/HOL/Import/import_rule.ML b/src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML
+++ b/src/HOL/Import/import_rule.ML
@@ -1,451 +1,451 @@
 (*  Title:      HOL/Import/import_rule.ML
     Author:     Cezary Kaliszyk, University of Innsbruck
     Author:     Alexander Krauss, QAware GmbH
 
 Importer proof rules and processing of lines and files.
 
 Based on earlier code by Steven Obua and Sebastian Skalberg.
 *)
 
 signature IMPORT_RULE =
 sig
   val beta : cterm -> thm
   val eq_mp : thm -> thm -> thm
   val comb : thm -> thm -> thm
   val trans : thm -> thm -> thm
   val deduct : thm -> thm -> thm
   val conj1 : thm -> thm
   val conj2 : thm -> thm
   val refl : cterm -> thm
   val abs : cterm -> thm -> thm
   val mdef : string -> theory -> thm
   val def : string -> cterm -> theory -> thm * theory
   val mtydef : string -> theory -> thm
   val tydef :
     string -> string -> string -> cterm -> cterm -> thm -> theory -> thm * theory
   val inst_type : (ctyp * ctyp) list -> thm -> theory -> thm
   val inst : (cterm * cterm) list -> thm -> thm
 
   type state
   val init_state : state
   val process_line : string -> (theory * state) -> (theory * state)
   val process_file : Path.T -> theory -> theory
 end
 
 structure Import_Rule: IMPORT_RULE =
 struct
 
 val init_state = ((Inttab.empty, 0), (Inttab.empty, 0), (Inttab.empty, 0))
 
 type state = (ctyp Inttab.table * int) * (cterm Inttab.table * int) * (thm Inttab.table * int)
 
 fun implies_elim_all th = implies_elim_list th (map Thm.assume (cprems_of th))
 
 fun meta_mp th1 th2 =
   let
     val th1a = implies_elim_all th1
     val th1b = Thm.implies_intr (strip_imp_concl (Thm.cprop_of th2)) th1a
     val th2a = implies_elim_all th2
     val th3 = Thm.implies_elim th1b th2a
   in
     implies_intr_hyps th3
   end
 
 fun meta_eq_to_obj_eq th =
   let
     val (tml, tmr) = Thm.dest_binop (strip_imp_concl (Thm.cprop_of th))
     val cty = Thm.ctyp_of_cterm tml
     val i = Thm.instantiate' [SOME cty] [SOME tml, SOME tmr]
       @{thm meta_eq_to_obj_eq}
   in
     Thm.implies_elim i th
   end
 
 fun beta ct = meta_eq_to_obj_eq (Thm.beta_conversion false ct)
 
 fun eq_mp th1 th2 =
   let
     val (tm1l, tm1r) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1)))
     val i1 = Thm.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
     val i2 = meta_mp i1 th1
   in
     meta_mp i2 th2
   end
 
 fun comb th1 th2 =
   let
     val t1c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1))
     val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
     val (cf, cg) = Thm.dest_binop t1c
     val (cx, cy) = Thm.dest_binop t2c
     val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_cterm cf)
     val i1 = Thm.instantiate' [SOME fd, SOME fr]
       [SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong}
     val i2 = meta_mp i1 th1
   in
     meta_mp i2 th2
   end
 
 fun trans th1 th2 =
   let
     val t1c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1))
     val t2c = Thm.dest_arg (strip_imp_concl (Thm.cprop_of th2))
     val (r, s) = Thm.dest_binop t1c
     val (_, t) = Thm.dest_binop t2c
     val ty = Thm.ctyp_of_cterm r
     val i1 = Thm.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
     val i2 = meta_mp i1 th1
   in
     meta_mp i2 th2
   end
 
 fun deduct th1 th2 =
   let
     val th1c = strip_imp_concl (Thm.cprop_of th1)
     val th2c = strip_imp_concl (Thm.cprop_of th2)
     val th1a = implies_elim_all th1
     val th2a = implies_elim_all th2
     val th1b = Thm.implies_intr th2c th1a
     val th2b = Thm.implies_intr th1c th2a
     val i = Thm.instantiate' []
       [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
     val i1 = Thm.implies_elim i (Thm.assume (Thm.cprop_of th2b))
     val i2 = Thm.implies_elim i1 th1b
     val i3 = Thm.implies_intr (Thm.cprop_of th2b) i2
     val i4 = Thm.implies_elim i3 th2b
   in
     implies_intr_hyps i4
   end
 
 fun conj1 th =
   let
     val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
     val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
   in
     meta_mp i th
   end
 
 fun conj2 th =
   let
     val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
     val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
   in
     meta_mp i th
   end
 
 fun refl ctm =
   let
     val cty = Thm.ctyp_of_cterm ctm
   in
     Thm.instantiate' [SOME cty] [SOME ctm] @{thm refl}
   end
 
 fun abs cv th =
   let
     val th1 = implies_elim_all th
     val (tl, tr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1)))
     val (ll, lr) = (Thm.lambda cv tl, Thm.lambda cv tr)
     val (al, ar) = (Thm.apply ll cv, Thm.apply lr cv)
     val bl = beta al
     val br = meta_eq_to_obj_eq (Thm.symmetric (Thm.beta_conversion false ar))
     val th2 = trans (trans bl th1) br
     val th3 = implies_elim_all th2
     val th4 = Thm.forall_intr cv th3
     val i = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
       [SOME ll, SOME lr] @{thm ext2}
   in
     meta_mp i th4
   end
 
 fun freezeT thy thm =
   let
     val tvars = Term.add_tvars (Thm.prop_of thm) []
     val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars
   in
     Thm.instantiate (TVars.make (tvars ~~ map (Thm.global_ctyp_of thy) tfrees), Vars.empty) thm
   end
 
 fun def' constname rhs thy =
   let
     val rhs = Thm.term_of rhs
     val typ = type_of rhs
     val constbinding = Binding.name constname
     val thy1 = Sign.add_consts [(constbinding, typ, NoSyn)] thy
     val eq = Logic.mk_equals (Const (Sign.full_name thy1 constbinding, typ), rhs)
     val (thms, thy2) = Global_Theory.add_defs false
       [((Binding.suffix_name "_hldef" constbinding, eq), [])] thy1
     val def_thm = freezeT thy1 (hd thms)
   in
     (meta_eq_to_obj_eq def_thm, thy2)
   end
 
 fun mdef name thy =
   case Import_Data.get_const_def name thy of
     SOME th => th
   | NONE => error ("constant mapped but no definition: " ^ name)
 
 fun def constname rhs thy =
   case Import_Data.get_const_def constname thy of
     SOME _ =>
       let
         val () = warning ("Const mapped but def provided: " ^ constname)
       in
         (mdef constname thy, thy)
       end
   | NONE => def' constname rhs thy
 
 fun typedef_hollight th thy =
   let
     val (th_s, cn) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
     val (th_s, abst) = Thm.dest_comb th_s
     val rept = Thm.dest_arg th_s
     val P = Thm.dest_arg cn
     val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
   in
     Thm.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
       SOME (Thm.global_cterm_of thy (Free ("a", Thm.typ_of nty))),
       SOME (Thm.global_cterm_of thy (Free ("r", Thm.typ_of oty)))] @{thm typedef_hol2hollight}
   end
 
 fun tydef' tycname abs_name rep_name cP ct td_th thy =
   let
     val ctT = Thm.ctyp_of_cterm ct
     val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
     val th2 = meta_mp nonempty td_th
     val c =
       case Thm.concl_of th2 of
         _ $ (Const(\<^const_name>\<open>Ex\<close>,_) $ Abs(_,_,Const(\<^const_name>\<open>Set.member\<close>,_) $ _ $ c)) => c
       | _ => error "type_introduction: bad type definition theorem"
     val tfrees = Term.add_tfrees c []
     val tnames = sort_strings (map fst tfrees)
     val typedef_bindings =
      {Rep_name = Binding.name rep_name,
       Abs_name = Binding.name abs_name,
       type_definition_name = Binding.name ("type_definition_" ^ tycname)}
     val ((_, typedef_info), thy') =
      Named_Target.theory_map_result (apsnd o Typedef.transform_info)
      (Typedef.add_typedef {overloaded = false}
        (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
        (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1)) thy
     val aty = #abs_type (#1 typedef_info)
     val th = freezeT thy' (#type_definition (#2 typedef_info))
     val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
     val (th_s, abst) = Thm.dest_comb th_s
     val rept = Thm.dest_arg th_s
     val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
     val typedef_th =
        Thm.instantiate'
           [SOME nty, SOME oty]
           [SOME rept, SOME abst, SOME cP, SOME (Thm.global_cterm_of thy' (Free ("a", aty))),
              SOME (Thm.global_cterm_of thy' (Free ("r", Thm.typ_of ctT)))]
           @{thm typedef_hol2hollight}
     val th4 = typedef_th OF [#type_definition (#2 typedef_info)]
   in
     (th4, thy')
   end
 
 fun mtydef name thy =
   case Import_Data.get_typ_def name thy of
     SOME thn => meta_mp (typedef_hollight thn thy) thn
   | NONE => error ("type mapped but no tydef thm registered: " ^ name)
 
 fun tydef tycname abs_name rep_name P t td_th thy =
   case Import_Data.get_typ_def tycname thy of
     SOME _ =>
       let
         val () = warning ("Type mapped but proofs provided: " ^ tycname)
       in
         (mtydef tycname thy, thy)
       end
   | NONE => tydef' tycname abs_name rep_name P t td_th thy
 
 fun inst_type lambda th thy =
   let
     fun assoc _ [] = error "assoc"
       | assoc x ((x',y)::rest) = if x = x' then y else assoc x rest
     val lambda = map (fn (a, b) => (Thm.typ_of a, b)) lambda
     val tys_before = Term.add_tfrees (Thm.prop_of th) []
     val th1 = Thm.varifyT_global th
     val tys_after = Term.add_tvars (Thm.prop_of th1) []
     val tyinst =
       map2 (fn bef => fn iS =>
         (case try (assoc (TFree bef)) lambda of
           SOME cty => (iS, cty)
         | NONE => (iS, Thm.global_ctyp_of thy (TFree bef))))
       tys_before tys_after
   in
     Thm.instantiate (TVars.make tyinst, Vars.empty) th1
   end
 
 fun inst sigma th =
   let
     val (dom, rng) = ListPair.unzip (rev sigma)
   in
     th |> forall_intr_list dom
        |> forall_elim_list rng
   end
 
 fun transl_dotc #"." = "dot"
   | transl_dotc c = Char.toString c
 val transl_dot = String.translate transl_dotc
 
 fun transl_qmc #"?" = "t"
   | transl_qmc c = Char.toString c
 val transl_qm = String.translate transl_qmc
 
 fun getconstname s thy =
   case Import_Data.get_const_map s thy of
       SOME s => s
     | NONE => Sign.full_name thy (Binding.name (transl_dot s))
 fun gettyname s thy =
   case Import_Data.get_typ_map s thy of
     SOME s => s
   | NONE => Sign.full_name thy (Binding.name s)
 
 fun get (map, no) s =
   case Int.fromString s of
     NONE => error "Import_Rule.get: not a number"
   | SOME i => (case Inttab.lookup map (Int.abs i) of
       NONE => error "Import_Rule.get: lookup failed"
     | SOME res => (res, (if i < 0 then Inttab.delete (Int.abs i) map else map, no)))
 
 fun getty i (thy, (tyi, tmi, thi)) = let val (i, tyi) = (get tyi i) in (i, (thy, (tyi, tmi, thi))) end
 fun gettm i (thy, (tyi, tmi, thi)) = let val (i, tmi) = (get tmi i) in (i, (thy, (tyi, tmi, thi))) end
 fun getth i (thy, (tyi, tmi, thi)) = let val (i, thi) = (get thi i) in (i, (thy, (tyi, tmi, thi))) end
 fun set (map, no) v = (Inttab.update_new (no + 1, v) map, no + 1)
 fun setty v (thy, (tyi, tmi, thi)) = (thy, (set tyi v, tmi, thi))
 fun settm v (thy, (tyi, tmi, thi)) = (thy, (tyi, set tmi v, thi))
 fun setth v (thy, (tyi, tmi, thi)) = (thy, (tyi, tmi, set thi v))
 
 fun last_thm (_, _, (map, no)) =
   case Inttab.lookup map no of
     NONE => error "Import_Rule.last_thm: lookup failed"
   | SOME thm => thm
 
 fun listLast (h1 :: (h2 :: t)) = apfst (fn t => h1 :: h2 :: t) (listLast t)
   | listLast [p] = ([], p)
   | listLast [] = error "listLast: empty"
 
 fun pairList (h1 :: (h2 :: t)) = ((h1, h2) :: pairList t)
   | pairList [] = []
   | pairList _ = error "pairList: odd list length"
 
 fun store_thm binding thm thy =
   let
     val ctxt = Proof_Context.init_global thy
     val thm = Drule.export_without_context_open thm
     val tvs = Term.add_tvars (Thm.prop_of thm) []
     val tns = map (fn (_, _) => "'") tvs
     val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
     val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
     val thm' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) thm
   in
     snd (Global_Theory.add_thm ((binding, thm'), []) thy)
   end
 
 fun log_timestamp () =
   let
     val time = Time.now ()
     val millis = nth (space_explode "." (Time.fmt 3 time)) 1
   in
     Date.fmt "%d.%m.%Y %H:%M:%S." (Date.fromTimeLocal time) ^ millis
   end
 
 fun process_line str tstate =
   let
     fun process tstate (#"R", [t]) = gettm t tstate |>> refl |-> setth
       | process tstate (#"B", [t]) = gettm t tstate |>> beta |-> setth
       | process tstate (#"1", [th]) = getth th tstate |>> conj1 |-> setth
       | process tstate (#"2", [th]) = getth th tstate |>> conj2 |-> setth
       | process tstate (#"H", [t]) =
           gettm t tstate |>> Thm.apply \<^cterm>\<open>Trueprop\<close> |>> Thm.trivial |-> setth
       | process tstate (#"A", [_, t]) =
           gettm t tstate |>> Thm.apply \<^cterm>\<open>Trueprop\<close> |>> Skip_Proof.make_thm_cterm |-> setth
       | process tstate (#"C", [th1, th2]) =
           getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => comb t1 t2) |-> setth
       | process tstate (#"T", [th1, th2]) =
           getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => trans t1 t2) |-> setth
       | process tstate (#"E", [th1, th2]) =
           getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => eq_mp t1 t2) |-> setth
       | process tstate (#"D", [th1, th2]) =
           getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => deduct t1 t2) |-> setth
       | process tstate (#"L", [t, th]) =
           gettm t tstate ||>> (fn ti => getth th ti) |>> (fn (tm, th) => abs tm th) |-> setth
       | process (thy, state) (#"M", [s]) =
           let
             val ctxt = Proof_Context.init_global thy
             val thm = freezeT thy (Global_Theory.get_thm thy s)
             val ((_, [th']), _) = Variable.import true [thm] ctxt
           in
             setth th' (thy, state)
           end
       | process (thy, state) (#"Q", l) =
           let
             val (tys, th) = listLast l
             val (th, tstate) = getth th (thy, state)
             val (tys, tstate) = fold_map getty tys tstate
           in
             setth (inst_type (pairList tys) th thy) tstate
           end
       | process tstate (#"S", l) =
           let
             val (tms, th) = listLast l
             val (th, tstate) = getth th tstate
             val (tms, tstate) = fold_map gettm tms tstate
           in
             setth (inst (pairList tms) th) tstate
           end
       | process tstate (#"F", [name, t]) =
           let
             val (tm, (thy, state)) = gettm t tstate
             val (th, thy) = def (transl_dot name) tm thy
           in
             setth th (thy, state)
           end
       | process (thy, state) (#"F", [name]) = setth (mdef name thy) (thy, state)
       | process tstate (#"Y", [name, absname, repname, t1, t2, th]) =
           let
             val (th, tstate) = getth th tstate
             val (t1, tstate) = gettm t1 tstate
             val (t2, (thy, state)) = gettm t2 tstate
             val (th, thy) = tydef name absname repname t1 t2 th thy
           in
             setth th (thy, state)
           end
       | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state)
       | process (thy, state) (#"t", [n]) =
           setty (Thm.global_ctyp_of thy (TFree ("'" ^ (transl_qm n), \<^sort>\<open>type\<close>))) (thy, state)
       | process (thy, state) (#"a", n :: l) =
           fold_map getty l (thy, state) |>>
             (fn tys => Thm.global_ctyp_of thy (Type (gettyname n thy, map Thm.typ_of tys))) |-> setty
       | process (thy, state) (#"v", [n, ty]) =
           getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (Free (transl_dot n, Thm.typ_of ty))) |-> settm
       | process (thy, state) (#"c", [n, ty]) =
           getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (Const (getconstname n thy, Thm.typ_of ty))) |-> settm
       | process tstate (#"f", [t1, t2]) =
           gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.apply t1 t2) |-> settm
       | process tstate (#"l", [t1, t2]) =
           gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm
       | process (thy, state) (#"+", [s]) =
           (store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state)
       | process _ (c, _) = error ("process: unknown command: " ^ String.implode [c])
 
     fun parse_line s =
         case String.tokens (fn x => (x = #"\n" orelse x = #" ")) s of
           [] => error "parse_line: empty"
         | h :: t => (case String.explode h of
             [] => error "parse_line: empty command"
           | sh :: st => (sh, (String.implode st) :: t))
   in
     process tstate (parse_line str)
   end
 
 fun process_file path thy =
-  (thy, init_state) |> File.fold_lines process_line path |> fst
+  #1 (fold process_line (File.read_lines path) (thy, init_state))
 
 val _ = Outer_Syntax.command \<^command_keyword>\<open>import_file\<close>
   "import a recorded proof file"
   (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
 
 
 end
diff --git a/src/HOL/Tools/sat_solver.ML b/src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML
+++ b/src/HOL/Tools/sat_solver.ML
@@ -1,1033 +1,1033 @@
 (*  Title:      HOL/Tools/sat_solver.ML
     Author:     Tjark Weber
     Copyright   2004-2009
 
 Interface to external SAT solvers, and (simple) built-in SAT solvers.
 
 Relevant Isabelle environment settings:
 
   # MiniSat 1.14
   #MINISAT_HOME=/usr/local/bin
 
   # zChaff
   #ZCHAFF_HOME=/usr/local/bin
 
   # BerkMin561
   #BERKMIN_HOME=/usr/local/bin
   #BERKMIN_EXE=BerkMin561-linux
   #BERKMIN_EXE=BerkMin561-solaris
 
   # Jerusat 1.3
   #JERUSAT_HOME=/usr/local/bin
 *)
 
 signature SAT_SOLVER =
 sig
   exception NOT_CONFIGURED
 
   type assignment = int -> bool option
   type proof      = int list Inttab.table * int
   datatype result = SATISFIABLE of assignment
                   | UNSATISFIABLE of proof option
                   | UNKNOWN
   type solver     = Prop_Logic.prop_formula -> result
 
   (* auxiliary functions to create external SAT solvers *)
   val write_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula -> unit
   val write_dimacs_sat_file : Path.T -> Prop_Logic.prop_formula -> unit
   val read_std_result_file : Path.T -> string * string * string -> result
   val make_external_solver : string -> (Prop_Logic.prop_formula -> unit) ->
     (unit -> result) -> solver
 
   val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula
 
   (* generic solver interface *)
   val get_solvers   : unit -> (string * solver) list
   val add_solver    : string * solver -> unit
   val invoke_solver : string -> solver  (* exception Option *)
 end;
 
 structure SAT_Solver : SAT_SOLVER =
 struct
 
   open Prop_Logic;
 
 (* ------------------------------------------------------------------------- *)
 (* should be raised by an external SAT solver to indicate that the solver is *)
 (* not configured properly                                                   *)
 (* ------------------------------------------------------------------------- *)
 
   exception NOT_CONFIGURED;
 
 (* ------------------------------------------------------------------------- *)
 (* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is  *)
 (*      a satisfying assignment regardless of the value of variable 'i'      *)
 (* ------------------------------------------------------------------------- *)
 
   type assignment = int -> bool option;
 
 (* ------------------------------------------------------------------------- *)
 (* a proof of unsatisfiability, to be interpreted as follows: each integer   *)
 (*      is a clause ID, each list 'xs' stored under the key 'x' in the table *)
 (*      contains the IDs of clauses that must be resolved (in the given      *)
 (*      order) to obtain the new clause 'x'.  Each list 'xs' must be         *)
 (*      non-empty, and the literal to be resolved upon must always be unique *)
 (*      (e.g. "A | ~B" must not be resolved with "~A | B").  Circular        *)
 (*      dependencies of clauses are not allowed.  (At least) one of the      *)
 (*      clauses in the table must be the empty clause (i.e. contain no       *)
 (*      literals); its ID is given by the second component of the proof.     *)
 (*      The clauses of the original problem passed to the SAT solver have    *)
 (*      consecutive IDs starting with 0.  Clause IDs must be non-negative,   *)
 (*      but do not need to be consecutive.                                   *)
 (* ------------------------------------------------------------------------- *)
 
   type proof = int list Inttab.table * int;
 
 (* ------------------------------------------------------------------------- *)
 (* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying  *)
 (*      assignment must be returned as well; if the result is                *)
 (*      'UNSATISFIABLE', a proof of unsatisfiability may be returned         *)
 (* ------------------------------------------------------------------------- *)
 
   datatype result = SATISFIABLE of assignment
                   | UNSATISFIABLE of proof option
                   | UNKNOWN;
 
 (* ------------------------------------------------------------------------- *)
 (* type of SAT solvers: given a propositional formula, a satisfying          *)
 (*      assignment may be returned                                           *)
 (* ------------------------------------------------------------------------- *)
 
   type solver = prop_formula -> result;
 
 (* ------------------------------------------------------------------------- *)
 (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic   *)
 (*      to a file in DIMACS CNF format (see "Satisfiability Suggested        *)
 (*      Format", May 8 1993, Section 2.1)                                    *)
 (* Note: 'fm' must not contain a variable index less than 1.                 *)
 (* Note: 'fm' must be given in CNF.                                          *)
 (* ------------------------------------------------------------------------- *)
 
   fun write_dimacs_cnf_file path fm =
   let
     fun cnf_True_False_elim True =
       Or (BoolVar 1, Not (BoolVar 1))
       | cnf_True_False_elim False =
       And (BoolVar 1, Not (BoolVar 1))
       | cnf_True_False_elim fm =
       fm  (* since 'fm' is in CNF, either 'fm'='True'/'False',
              or 'fm' does not contain 'True'/'False' at all *)
     fun cnf_number_of_clauses (And (fm1, fm2)) =
       (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
       | cnf_number_of_clauses _ =
       1
     fun write_cnf_file out =
     let
       fun write_formula True =
           error "formula is not in CNF"
         | write_formula False =
           error "formula is not in CNF"
         | write_formula (BoolVar i) =
           (i>=1 orelse error "formula contains a variable index less than 1";
-           File.output out (string_of_int i))
+           File_Stream.output out (string_of_int i))
         | write_formula (Not (BoolVar i)) =
-          (File.output out "-";
+          (File_Stream.output out "-";
            write_formula (BoolVar i))
         | write_formula (Not _) =
           error "formula is not in CNF"
         | write_formula (Or (fm1, fm2)) =
           (write_formula fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula fm2)
         | write_formula (And (fm1, fm2)) =
           (write_formula fm1;
-           File.output out " 0\n";
+           File_Stream.output out " 0\n";
            write_formula fm2)
       val fm'               = cnf_True_False_elim fm
       val number_of_vars    = maxidx fm'
       val number_of_clauses = cnf_number_of_clauses fm'
     in
-      File.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n";
-      File.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^
+      File_Stream.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n";
+      File_Stream.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^
                             string_of_int number_of_clauses ^ "\n");
       write_formula fm';
-      File.output out " 0\n"
+      File_Stream.output out " 0\n"
     end
   in
-    File.open_output write_cnf_file path
+    File_Stream.open_output write_cnf_file path
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic   *)
 (*      to a file in DIMACS SAT format (see "Satisfiability Suggested        *)
 (*      Format", May 8 1993, Section 2.2)                                    *)
 (* Note: 'fm' must not contain a variable index less than 1.                 *)
 (* ------------------------------------------------------------------------- *)
 
   fun write_dimacs_sat_file path fm =
   let
     fun write_sat_file out =
     let
       fun write_formula True =
-          File.output out "*()"
+          File_Stream.output out "*()"
         | write_formula False =
-          File.output out "+()"
+          File_Stream.output out "+()"
         | write_formula (BoolVar i) =
           (i>=1 orelse error "formula contains a variable index less than 1";
-           File.output out (string_of_int i))
+           File_Stream.output out (string_of_int i))
         | write_formula (Not (BoolVar i)) =
-          (File.output out "-";
+          (File_Stream.output out "-";
            write_formula (BoolVar i))
         | write_formula (Not fm) =
-          (File.output out "-(";
+          (File_Stream.output out "-(";
            write_formula fm;
-           File.output out ")")
+           File_Stream.output out ")")
         | write_formula (Or (fm1, fm2)) =
-          (File.output out "+(";
+          (File_Stream.output out "+(";
            write_formula_or fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula_or fm2;
-           File.output out ")")
+           File_Stream.output out ")")
         | write_formula (And (fm1, fm2)) =
-          (File.output out "*(";
+          (File_Stream.output out "*(";
            write_formula_and fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula_and fm2;
-           File.output out ")")
+           File_Stream.output out ")")
       (* optimization to make use of n-ary disjunction/conjunction *)
       and write_formula_or (Or (fm1, fm2)) =
           (write_formula_or fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula_or fm2)
         | write_formula_or fm =
           write_formula fm
       and write_formula_and (And (fm1, fm2)) =
           (write_formula_and fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula_and fm2)
         | write_formula_and fm =
           write_formula fm
       val number_of_vars = Int.max (maxidx fm, 1)
     in
-      File.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n";
-      File.output out ("p sat " ^ string_of_int number_of_vars ^ "\n");
-      File.output out "(";
+      File_Stream.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n";
+      File_Stream.output out ("p sat " ^ string_of_int number_of_vars ^ "\n");
+      File_Stream.output out "(";
       write_formula fm;
-      File.output out ")\n"
+      File_Stream.output out ")\n"
     end
   in
-    File.open_output write_sat_file path
+    File_Stream.open_output write_sat_file path
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* read_std_result_file: scans a SAT solver's output file for a satisfying   *)
 (*      variable assignment.  Returns the assignment, or 'UNSATISFIABLE' if  *)
 (*      the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *)
 (*      neither 'satisfiable' nor 'unsatisfiable'.  Empty lines are ignored. *)
 (*      The assignment must be given in one or more lines immediately after  *)
 (*      the line that contains 'satisfiable'.  These lines must begin with   *)
 (*      'assignment_prefix'.  Variables must be separated by " ".  Non-      *)
 (*      integer strings are ignored.  If variable i is contained in the      *)
 (*      assignment, then i is interpreted as 'true'.  If ~i is contained in  *)
 (*      the assignment, then i is interpreted as 'false'.  Otherwise the     *)
 (*      value of i is taken to be unspecified.                               *)
 (* ------------------------------------------------------------------------- *)
 
   fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
   let
     fun int_list_from_string s =
       map_filter Int.fromString (space_explode " " s)
     fun assignment_from_list [] i =
       NONE  (* the SAT solver didn't provide a value for this variable *)
       | assignment_from_list (x::xs) i =
       if x=i then (SOME true)
       else if x=(~i) then (SOME false)
       else assignment_from_list xs i
     fun parse_assignment xs [] =
       assignment_from_list xs
       | parse_assignment xs (line::lines) =
       if String.isPrefix assignment_prefix line then
         parse_assignment (xs @ int_list_from_string line) lines
       else
         assignment_from_list xs
     fun is_substring needle haystack =
     let
       val length1 = String.size needle
       val length2 = String.size haystack
     in
       if length2 < length1 then
         false
       else if needle = String.substring (haystack, 0, length1) then
         true
       else is_substring needle (String.substring (haystack, 1, length2-1))
     end
     fun parse_lines [] =
       UNKNOWN
       | parse_lines (line::lines) =
       if is_substring unsatisfiable line then
         UNSATISFIABLE NONE
       else if is_substring satisfiable line then
         SATISFIABLE (parse_assignment [] lines)
       else
         parse_lines lines
   in
     (parse_lines o filter (fn l => l <> "") o split_lines o File.read) path
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn'        *)
 (* ------------------------------------------------------------------------- *)
 
   fun make_external_solver cmd writefn readfn fm =
     (writefn fm; Isabelle_System.bash cmd; readfn ());
 
 (* ------------------------------------------------------------------------- *)
 (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *)
 (*      a SAT problem given in DIMACS CNF format                             *)
 (* ------------------------------------------------------------------------- *)
 
   fun read_dimacs_cnf_file path =
   let
     fun filter_preamble [] =
       error "problem line not found in DIMACS CNF file"
       | filter_preamble (line::lines) =
       if String.isPrefix "c " line orelse line = "c" then
         (* ignore comments *)
         filter_preamble lines
       else if String.isPrefix "p " line then
         (* ignore the problem line (which must be the last line of the preamble) *)
         (* Ignoring the problem line implies that if the file contains more clauses *)
         (* or variables than specified in its preamble, we will accept it anyway.   *)
         lines
       else
         error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \""
     fun int_from_string s =
       case Int.fromString s of
         SOME i => i
       | NONE   => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number")
     fun clauses xs =
       let
         val (xs1, xs2) = chop_prefix (fn i => i <> 0) xs
       in
         case xs2 of
           []      => [xs1]
         | (0::[]) => [xs1]
         | (0::tl) => xs1 :: clauses tl
         | _       => raise Fail "SAT_Solver.clauses"
       end
     fun literal_from_int i =
       (i<>0 orelse error "variable index in DIMACS CNF file is 0";
       if i>0 then
         Prop_Logic.BoolVar i
       else
         Prop_Logic.Not (Prop_Logic.BoolVar (~i)))
     fun disjunction [] =
       error "empty clause in DIMACS CNF file"
       | disjunction (x::xs) =
       (case xs of
         [] => x
       | _  => Prop_Logic.Or (x, disjunction xs))
     fun conjunction [] =
       error "no clause in DIMACS CNF file"
       | conjunction (x::xs) =
       (case xs of
         [] => x
       | _  => Prop_Logic.And (x, conjunction xs))
   in
     (conjunction
     o (map disjunction)
     o (map (map literal_from_int))
     o clauses
     o (map int_from_string)
     o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"])))
     o filter_preamble
     o filter (fn l => l <> "")
     o split_lines
     o File.read)
       path
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* solvers: a table of all registered SAT solvers                            *)
 (* ------------------------------------------------------------------------- *)
 
   val solvers = Synchronized.var "solvers" ([] : (string * solver) list);
 
   fun get_solvers () = Synchronized.value solvers;
 
 (* ------------------------------------------------------------------------- *)
 (* add_solver: updates 'solvers' by adding a new solver                      *)
 (* ------------------------------------------------------------------------- *)
 
   fun add_solver (name, new_solver) =
     Synchronized.change solvers (fn the_solvers =>
       let
         val _ = if AList.defined (op =) the_solvers name
           then warning ("SAT solver " ^ quote name ^ " was defined before")
           else ();
       in AList.update (op =) (name, new_solver) the_solvers end);
 
 (* ------------------------------------------------------------------------- *)
 (* invoke_solver: returns the solver associated with the given 'name'        *)
 (* Note: If no solver is associated with 'name', exception 'Option' will be  *)
 (*       raised.                                                             *)
 (* ------------------------------------------------------------------------- *)
 
   fun invoke_solver name =
     the (AList.lookup (op =) (get_solvers ()) name);
 
 end;  (* SAT_Solver *)
 
 
 (* ------------------------------------------------------------------------- *)
 (* Predefined SAT solvers                                                    *)
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)
 (* Internal SAT solver, available as 'SAT_Solver.invoke_solver "cdclite"' --  *)
 (* a simplified implementation of the conflict-driven clause-learning        *)
 (* algorithm (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean       *)
 (* Satisfiability Solvers", July 2002, Fig. 2). This solver produces models  *)
 (* and proof traces.                                                         *)
 (* ------------------------------------------------------------------------- *)
 
 let
   type clause = int list * int
   type value = bool option
   datatype reason = Decided | Implied of clause | Level0 of int
   type variable = bool option * reason * int * int
   type proofs = int * int list Inttab.table
   type state =
     int * int list * variable Inttab.table * clause list Inttab.table * proofs
   exception CONFLICT of clause * state
   exception UNSAT of clause * state
 
   fun neg i = ~i
 
   fun lit_value lit value = if lit > 0 then value else Option.map not value
 
   fun var_of vars lit: variable = the (Inttab.lookup vars (abs lit))
   fun value_of vars lit = lit_value lit (#1 (var_of vars lit))
   fun reason_of vars lit = #2 (var_of vars lit)
   fun level_of vars lit = #3 (var_of vars lit)
 
   fun is_true vars lit = (value_of vars lit = SOME true)
   fun is_false vars lit = (value_of vars lit = SOME false)
   fun is_unassigned vars lit = (value_of vars lit = NONE)
   fun assignment_of vars lit = the_default NONE (try (value_of vars) lit)
 
   fun put_var value reason level (_, _, _, rank) = (value, reason, level, rank)
   fun incr_rank (value, reason, level, rank) = (value, reason, level, rank + 1)
   fun update_var lit f = Inttab.map_entry (abs lit) f
   fun add_var lit = Inttab.update (abs lit, (NONE, Decided, ~1, 0))
 
   fun assign lit r l = update_var lit (put_var (SOME (lit > 0)) r l)
   fun unassign lit = update_var lit (put_var NONE Decided ~1)
 
   fun add_proof [] (idx, ptab) = (idx, (idx + 1, ptab))
     | add_proof ps (idx, ptab) = (idx, (idx + 1, Inttab.update (idx, ps) ptab))
 
   fun level0_proof_of (Level0 idx) = SOME idx
     | level0_proof_of _ = NONE
 
   fun level0_proofs_of vars = map_filter (level0_proof_of o reason_of vars)
   fun prems_of vars (lits, p) = p :: level0_proofs_of vars lits
   fun mk_proof vars cls proofs = add_proof (prems_of vars cls) proofs
 
   fun push lit cls (level, trail, vars, clss, proofs) =
     let
       val (reason, proofs) =
         if level = 0 then apfst Level0 (mk_proof vars cls proofs)
         else (Implied cls, proofs)
     in (level, lit :: trail, assign lit reason level vars, clss, proofs) end
 
   fun push_decided lit (level, trail, vars, clss, proofs) =
     let val vars' = assign lit Decided (level + 1) vars
     in (level + 1, lit :: 0 :: trail, vars', clss, proofs) end
 
   fun prop (cls as (lits, _)) (cx as (units, state as (level, _, vars, _, _))) =
     if exists (is_true vars) lits then cx
     else if forall (is_false vars) lits then
       if level = 0 then raise UNSAT (cls, state)
       else raise CONFLICT (cls, state)
     else
       (case filter (is_unassigned vars) lits of
         [lit] => (lit :: units, push lit cls state)
       | _ => cx)
 
   fun propagate units (state as (_, _, _, clss, _)) =
     (case fold (fold prop o Inttab.lookup_list clss) units ([], state) of
       ([], state') => (NONE, state')
     | (units', state') => propagate units' state')
     handle CONFLICT (cls, state') => (SOME cls, state')
 
   fun max_unassigned (v, (NONE, _, _, rank)) (x as (_, r)) =
         if rank > r then (SOME v, rank) else x
     | max_unassigned _  x = x
 
   fun decide (state as (_, _, vars, _, _)) =
     (case Inttab.fold max_unassigned vars (NONE, 0) of
       (SOME lit, _) => SOME (lit, push_decided lit state)
     | (NONE, _) => NONE)
 
   fun mark lit = Inttab.update (abs lit, true)
   fun marked ms lit = the_default false (Inttab.lookup ms (abs lit))
   fun ignore l ms lit = ((lit = l) orelse marked ms lit)
 
   fun first_lit _ [] = raise Empty
     | first_lit _ (0 :: _) = raise Empty
     | first_lit pred (lit :: lits) =
         if pred lit then (lit, lits) else first_lit pred lits
 
   fun reason_cls_of vars lit =
     (case reason_of vars lit of
       Implied cls => cls
     | _ => raise Option)
 
   fun analyze conflicting_cls (level, trail, vars, _, _) =
     let
       fun back i lit (lits, p) trail ms ls ps =
         let
           val (lits0, lits') = List.partition (equal 0 o level_of vars) lits
           val lits1 = filter_out (ignore lit ms) lits'
           val lits2 = filter_out (equal level o level_of vars) lits1
           val i' = length lits1 - length lits2 + i
           val ms' = fold mark lits1 ms
           val ls' = lits2 @ ls
           val ps' = level0_proofs_of vars lits0 @ (p :: ps)
           val (lit', trail') = first_lit (marked ms') trail
         in 
           if i' = 1 then (neg lit', ls', rev ps')
           else back (i' - 1) lit' (reason_cls_of vars lit') trail' ms' ls' ps'
         end
     in back 0 0 conflicting_cls trail Inttab.empty [] [] end
 
   fun keep_clause (cls as (lits, _)) (level, trail, vars, clss, proofs) =
     let
       val vars' = fold (fn lit => update_var lit incr_rank) lits vars
       val clss' = fold (fn lit => Inttab.cons_list (neg lit, cls)) lits clss
     in (level, trail, vars', clss', proofs) end
 
   fun learn (cls as (lits, _)) = (length lits <= 2) ? keep_clause cls
 
   fun backjump _ (state as (_, [], _, _, _)) = state 
     | backjump i (level, 0 :: trail, vars, clss, proofs) =
         (level - 1, trail, vars, clss, proofs) |> (i > 1) ? backjump (i - 1)
     | backjump i (level, lit :: trail, vars, clss, proofs) =
         backjump i (level, trail, unassign lit vars, clss, proofs)
 
   fun search units state =
     (case propagate units state of
       (NONE, state' as (_, _, vars, _, _)) =>
         (case decide state' of
           NONE => SAT_Solver.SATISFIABLE (assignment_of vars)
         | SOME (lit, state'') => search [lit] state'')
     | (SOME conflicting_cls, state' as (level, trail, vars, clss, proofs)) =>
         let 
           val (lit, lits, ps) = analyze conflicting_cls state'
           val (idx, proofs') = add_proof ps proofs
           val cls = (lit :: lits, idx)
         in
           (level, trail, vars, clss, proofs')
           |> backjump (level - fold (Integer.max o level_of vars) lits 0)
           |> learn cls
           |> push lit cls
           |> search [lit]
         end)
 
   fun has_opposing_lits [] = false
     | has_opposing_lits (lit :: lits) =
         member (op =) lits (neg lit) orelse has_opposing_lits lits
 
   fun add_clause (cls as ([_], _)) (units, state) =
         let val (units', state') = prop cls (units, state)
         in (units', state') end
     | add_clause (cls as (lits, _)) (cx as (units, state)) =
         if has_opposing_lits lits then cx
         else (units, keep_clause cls state)
 
   fun mk_clause lits proofs =
     apfst (pair (distinct (op =) lits)) (add_proof [] proofs)
 
   fun solve litss =
     let
       val (clss, proofs) = fold_map mk_clause litss (0, Inttab.empty)
       val vars = fold (fold add_var) litss Inttab.empty
       val state = (0, [], vars, Inttab.empty, proofs)
     in uncurry search (fold add_clause clss ([], state)) end
     handle UNSAT (conflicting_cls, (_, _, vars, _, proofs)) =>
       let val (idx, (_, ptab)) = mk_proof vars conflicting_cls proofs
       in SAT_Solver.UNSATISFIABLE (SOME (ptab, idx)) end
 
   fun variable_of (Prop_Logic.BoolVar 0) = error "bad propositional variable"
     | variable_of (Prop_Logic.BoolVar i) = i
     | variable_of _ = error "expected formula in CNF"
   fun literal_of (Prop_Logic.Not fm) = neg (variable_of fm)
     | literal_of fm = variable_of fm
   fun clause_of (Prop_Logic.Or (fm1, fm2)) = clause_of fm1 @ clause_of fm2
     | clause_of fm = [literal_of fm]
   fun clauses_of (Prop_Logic.And (fm1, fm2)) = clauses_of fm1 @ clauses_of fm2
     | clauses_of Prop_Logic.True = [[1, ~1]]
     | clauses_of Prop_Logic.False = [[1], [~1]]
     | clauses_of fm = [clause_of fm]
 
   fun dpll_solver fm =
     let val fm' = if Prop_Logic.is_cnf fm then fm else Prop_Logic.defcnf fm
     in solve (clauses_of fm') end
 in
   SAT_Solver.add_solver ("cdclite", dpll_solver)
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* Internal SAT solver, available as 'SAT_Solver.invoke_solver "auto"': uses *)
 (* the last installed solver (other than "auto" itself) that does not raise  *)
 (* 'NOT_CONFIGURED'.  (However, the solver may return 'UNKNOWN'.)            *)
 (* ------------------------------------------------------------------------- *)
 
 let
   fun auto_solver fm =
   let
     fun loop [] =
       SAT_Solver.UNKNOWN
       | loop ((name, solver)::solvers) =
       if name="auto" then
         (* do not call solver "auto" from within "auto" *)
         loop solvers
       else (
         (* apply 'solver' to 'fm' *)
         solver fm
           handle SAT_Solver.NOT_CONFIGURED => loop solvers
       )
   in
     loop (SAT_Solver.get_solvers ())
   end
 in
   SAT_Solver.add_solver ("auto", auto_solver)
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* MiniSat 1.14                                                              *)
 (* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/)            *)
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)
 (* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *)
 (* Matthews, which can output ASCII proof traces.  Replaying binary proof    *)
 (* traces generated by MiniSat-p_v1.14 has _not_ been implemented.           *)
 (* ------------------------------------------------------------------------- *)
 
 (* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *)
 (* that the latter is preferred by the "auto" solver                         *)
 
 (* There is a complication that is dealt with in the code below: MiniSat     *)
 (* introduces IDs for original clauses in the proof trace.  It does not (in  *)
 (* general) follow the convention that the original clauses are numbered     *)
 (* from 0 to n-1 (where n is the number of clauses in the formula).          *)
 
 let
   exception INVALID_PROOF of string
   fun minisat_with_proofs fm =
   let
     val _          = if (getenv "MINISAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else ()
     val serial_str = serial_string ()
     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
     val proofpath  = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))
     val cmd        = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " -t " ^ File.bash_path proofpath ^ "> /dev/null"
     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath fm
     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT")
     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
     val cnf        = Prop_Logic.defcnf fm
     val result     = SAT_Solver.make_external_solver cmd writefn readfn cnf
     val _          = try File.rm inpath
     val _          = try File.rm outpath
   in  case result of
     SAT_Solver.UNSATISFIABLE NONE =>
     (let
       val proof_lines = (split_lines o File.read) proofpath
         handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
       (* representation of clauses as ordered lists of literals (with duplicates removed) *)
       fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) =
         Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
         | clause_to_lit_list (Prop_Logic.BoolVar i) =
         [i]
         | clause_to_lit_list (Prop_Logic.Not (Prop_Logic.BoolVar i)) =
         [~i]
         | clause_to_lit_list _ =
         raise INVALID_PROOF "Error: invalid clause in CNF formula."
       fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
         cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
         | cnf_number_of_clauses _ =
         1
       val number_of_clauses = cnf_number_of_clauses cnf
       (* int list array *)
       val clauses = Array.array (number_of_clauses, [])
       (* initialize the 'clauses' array *)
       fun init_array (Prop_Logic.And (fm1, fm2), n) =
         init_array (fm2, init_array (fm1, n))
         | init_array (fm, n) =
         (Array.update (clauses, n, clause_to_lit_list fm); n+1)
       val _ = init_array (cnf, 0)
       (* optimization for the common case where MiniSat "R"s clauses in their *)
       (* original order:                                                      *)
       val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1)
       (* search the 'clauses' array for the given list of literals 'lits', *)
       (* starting at index '!last_ref_clause + 1'                          *)
       fun original_clause_id lits =
       let
         fun original_clause_id_from index =
           if index = number_of_clauses then
             (* search from beginning again *)
             original_clause_id_from 0
           (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
           (* testing for equality should suffice -- barring duplicate literals     *)
           else if Array.sub (clauses, index) = lits then (
             (* success *)
             last_ref_clause := index;
             SOME index
           ) else if index = !last_ref_clause then
             (* failure *)
             NONE
           else
             (* continue search *)
             original_clause_id_from (index + 1)
       in
         original_clause_id_from (!last_ref_clause + 1)
       end
       fun int_from_string s =
         (case Int.fromString s of
           SOME i => i
         | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered)."))
       (* parse the proof file *)
       val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
       val empty_id      = Unsynchronized.ref ~1
       (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
       (* our proof format, where original clauses are numbered starting from 0  *)
       val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table)
       fun sat_to_proof id = (
         case Inttab.lookup (!clause_id_map) id of
           SOME id' => id'
         | NONE     => raise INVALID_PROOF ("Clause ID " ^ string_of_int id ^ " used, but not defined.")
       )
       val next_id = Unsynchronized.ref (number_of_clauses - 1)
       fun process_tokens [] =
         ()
         | process_tokens (tok::toks) =
         if tok="R" then (
           case toks of
             id::sep::lits =>
             let
               val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
               val cid      = int_from_string id
               val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
               val ls       = sort int_ord (map int_from_string lits)
               val proof_id = case original_clause_id ls of
                                SOME orig_id => orig_id
                              | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
             in
               (* extend the mapping of clause IDs with this newly defined ID *)
               clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
               (* the proof itself doesn't change *)
             end
           | _ =>
             raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
         ) else if tok="C" then (
           case toks of
             id::sep::ids =>
             let
               val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
               val cid      = int_from_string id
               val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
               (* ignore the pivot literals in MiniSat's trace *)
               fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
                 | unevens (x :: [])      = x :: []
                 | unevens (x :: _ :: xs) = x :: unevens xs
               val rs       = (map sat_to_proof o unevens o map int_from_string) ids
               (* extend the mapping of clause IDs with this newly defined ID *)
               val proof_id = Unsynchronized.inc next_id
               val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
                                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
             in
               (* update clause table *)
               clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
                 handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
             end
           | _ =>
             raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens."
         ) else if tok="D" then (
           case toks of
             [id] =>
             let
               val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
               val _ = sat_to_proof (int_from_string id)
             in
               (* simply ignore "D" *)
               ()
             end
           | _ =>
             raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
         ) else if tok="X" then (
           case toks of
             [id1, id2] =>
             let
               val _            = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
               val _            = sat_to_proof (int_from_string id1)
               val new_empty_id = sat_to_proof (int_from_string id2)
             in
               (* update conflict id *)
               empty_id := new_empty_id
             end
           | _ =>
             raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
         ) else
           raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
       fun process_lines [] =
         ()
         | process_lines (l::ls) = (
           process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
           process_lines ls
         )
       (* proof *)
       val _ = process_lines proof_lines
       val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
     in
       SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
     end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE))
   | result =>
     result
   end
 in
   SAT_Solver.add_solver ("minisat_with_proofs", minisat_with_proofs)
 end;
 
 let
   fun minisat fm =
   let
     val _          = if getenv "MINISAT_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else ()
     val serial_str = serial_string ()
     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
     val cmd        = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " > /dev/null"
     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT")
     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
     val result     = SAT_Solver.make_external_solver cmd writefn readfn fm
     val _          = try File.rm inpath
     val _          = try File.rm outpath
   in
     result
   end
 in
   SAT_Solver.add_solver ("minisat", minisat)
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* zChaff (https://www.princeton.edu/~chaff/zchaff.html)                      *)
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)
 (* 'zchaff_with_proofs' applies the "zchaff" prover to a formula, and if     *)
 (* zChaff finds that the formula is unsatisfiable, a proof of this is read   *)
 (* from a file "resolve_trace" that was generated by zChaff.  See the code   *)
 (* below for the expected format of the "resolve_trace" file.  Aside from    *)
 (* some basic syntactic checks, no verification of the proof is performed.   *)
 (* ------------------------------------------------------------------------- *)
 
 (* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so   *)
 (* that the latter is preferred by the "auto" solver                         *)
 
 let
   exception INVALID_PROOF of string
   fun zchaff_with_proofs fm =
   case SAT_Solver.invoke_solver "zchaff" fm of
     SAT_Solver.UNSATISFIABLE NONE =>
     (let
       (* FIXME File.tmp_path (!?) *)
       val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
         handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
       fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
             cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
         | cnf_number_of_clauses _ = 1
       fun int_from_string s = (
         case Int.fromString s of
           SOME i => i
         | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
       )
       (* parse the "resolve_trace" file *)
       val clause_offset = Unsynchronized.ref ~1
       val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
       val empty_id      = Unsynchronized.ref ~1
       fun process_tokens [] =
         ()
         | process_tokens (tok::toks) =
         if tok="CL:" then (
           case toks of
             id::sep::ids =>
             let
               val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
               val cid = int_from_string id
               val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
               val rs  = map int_from_string ids
             in
               (* update clause table *)
               clause_table := Inttab.update_new (cid, rs) (!clause_table)
                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
             end
           | _ =>
             raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens."
         ) else if tok="VAR:" then (
           case toks of
             id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
             let
               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
               (* set 'clause_offset' to the largest used clause ID *)
               val _   = if !clause_offset = ~1 then clause_offset :=
                 (case Inttab.max (!clause_table) of
                   SOME (id, _) => id
                 | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
                 else
                   ()
               val vid = int_from_string id
               val _   = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).")
               val _   = int_from_string levid
               val _   = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).")
               val _   = int_from_string valid
               val _   = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).")
               val aid = int_from_string anteid
               val _   = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).")
               val ls  = map int_from_string lits
               (* convert the data provided by zChaff to our resolution-style proof format *)
               (* each "VAR:" line defines a unit clause, the resolvents are implicitly    *)
               (* given by the literals in the antecedent clause                           *)
               (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *)
               val cid = !clause_offset + vid
               (* the low bit of each literal gives its sign (positive/negative), therefore  *)
               (* we have to divide each literal by 2 to obtain the proper variable ID; then *)
               (* we add '!clause_offset' to obtain the ID of the corresponding unit clause  *)
               val vids = filter (not_equal vid) (map (fn l => l div 2) ls)
               val rs   = aid :: map (fn v => !clause_offset + v) vids
             in
               (* update clause table *)
               clause_table := Inttab.update_new (cid, rs) (!clause_table)
                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
             end
           | _ =>
             raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens."
         ) else if tok="CONF:" then (
           case toks of
             id::sep::ids =>
             let
               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
               val cid = int_from_string id
               val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
               val ls  = map int_from_string ids
               (* the conflict clause must be resolved with the unit clauses *)
               (* for its literals to obtain the empty clause                *)
               val vids         = map (fn l => l div 2) ls
               val rs           = cid :: map (fn v => !clause_offset + v) vids
               val new_empty_id = the_default (!clause_offset) (Option.map fst (Inttab.max (!clause_table))) + 1
             in
               (* update clause table and conflict id *)
               clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.");
               empty_id     := new_empty_id
             end
           | _ =>
             raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
         ) else
           raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
       fun process_lines [] =
         ()
         | process_lines (l::ls) = (
           process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
           process_lines ls
         )
       (* proof *)
       val _ = process_lines proof_lines
       val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
     in
       SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
     end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE))
   | result =>
     result
 in
   SAT_Solver.add_solver ("zchaff_with_proofs", zchaff_with_proofs)
 end;
 
 let
   fun zchaff fm =
   let
     val _          = if getenv "ZCHAFF_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else ()
     val serial_str = serial_string ()
     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
     val cmd        = "\"$ZCHAFF_HOME/zchaff\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath
     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
     val result     = SAT_Solver.make_external_solver cmd writefn readfn fm
     val _          = try File.rm inpath
     val _          = try File.rm outpath
   in
     result
   end
 in
   SAT_Solver.add_solver ("zchaff", zchaff)
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* BerkMin 561 (http://eigold.tripod.com/BerkMin.html)                       *)
 (* ------------------------------------------------------------------------- *)
 
 let
   fun berkmin fm =
   let
     val _          = if (getenv "BERKMIN_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else ()
     val serial_str = serial_string ()
     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
     val cmd        = "\"$BERKMIN_HOME/${BERKMIN_EXE:-BerkMin561}\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath
     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
     val result     = SAT_Solver.make_external_solver cmd writefn readfn fm
     val _          = try File.rm inpath
     val _          = try File.rm outpath
   in
     result
   end
 in
   SAT_Solver.add_solver ("berkmin", berkmin)
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/)                              *)
 (* ------------------------------------------------------------------------- *)
 
 let
   fun jerusat fm =
   let
     val _          = if (getenv "JERUSAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else ()
     val serial_str = serial_string ()
     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
     val cmd        = "\"$JERUSAT_HOME/Jerusat1.3\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath
     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
     val result     = SAT_Solver.make_external_solver cmd writefn readfn fm
     val _          = try File.rm inpath
     val _          = try File.rm outpath
   in
     result
   end
 in
   SAT_Solver.add_solver ("jerusat", jerusat)
 end;
diff --git a/src/Pure/General/bytes.ML b/src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML
+++ b/src/Pure/General/bytes.ML
@@ -1,221 +1,221 @@
 (*  Title:      Pure/General/bytes.ML
     Author:     Makarius
 
 Scalable byte strings, with incremental construction (add content to the
 end).
 
 Note: type string is implicitly limited by String.maxSize (approx. 64 MB on
 64_32 architecture).
 *)
 
 signature BYTES =
 sig
   val chunk_size: int
   type T
   val eq: T * T -> bool
   val length: T -> int
   val contents: T -> string list
   val contents_blob: T -> XML.body
   val content: T -> string
   val is_empty: T -> bool
   val empty: T
   val build: (T -> T) -> T
   val add_substring: substring -> T -> T
   val add: string -> T -> T
   val beginning: int -> T -> string
   val exists_string: (string -> bool) -> T -> bool
   val forall_string: (string -> bool) -> T -> bool
   val last_string: T -> string option
   val trim_line: T -> T
   val append: T -> T -> T
   val appends: T list -> T
   val string: string -> T
   val newline: T
   val buffer: Buffer.T -> T
   val space_explode: string -> T -> string list
   val split_lines: T -> string list
   val trim_split_lines: T -> string list
   val cat_lines: string list -> T
   val read_block: int -> BinIO.instream -> string
   val read_stream: int -> BinIO.instream -> T
   val write_stream: BinIO.outstream -> T -> unit
   val read: Path.T -> T
   val write: Path.T -> T -> unit
 end;
 
 structure Bytes: BYTES =
 struct
 
 (* primitive operations *)
 
 val chunk_size = 1024 * 1024;
 
 abstype T = Bytes of
   {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)}
 with
 
 fun length (Bytes {m, n, ...}) = m + n;
 
 val compact = implode o rev;
 
 fun eq (Bytes {buffer, chunks, m, n}, Bytes {buffer = buffer', chunks = chunks', m = m', n = n'}) =
   m = m' andalso n = n' andalso chunks = chunks' andalso
   (buffer = buffer' orelse compact buffer = compact buffer);
 
 fun contents (Bytes {buffer, chunks, ...}) =
   rev (chunks |> not (null buffer) ? cons (compact buffer));
 
 val contents_blob = contents #> XML.blob;
 
 val content = implode o contents;
 
 fun is_empty bytes = length bytes = 0;
 
 val empty = Bytes {buffer = [], chunks = [], m = 0, n = 0};
 
 fun build (f: T -> T) = f empty;
 
 fun add_substring s (bytes as Bytes {buffer, chunks, m, n}) =
   if Substring.isEmpty s then bytes
   else
     let val l = Substring.size s in
       if l + m < chunk_size
       then Bytes {buffer = Substring.string s :: buffer, chunks = chunks, m = l + m, n = n}
       else
         let
           val k = chunk_size - m;
           val chunk = compact (Substring.string (Substring.slice (s, 0, SOME k)) :: buffer);
           val s' = Substring.slice (s, k, SOME (l - k));
           val bytes' = Bytes {buffer = [], chunks = chunk :: chunks, m = 0, n = chunk_size + n};
         in add_substring s' bytes' end
     end;
 
 val add = add_substring o Substring.full;
 
 fun exists_string pred (Bytes {buffer, chunks, ...}) =
   let val ex = (exists o Library.exists_string) pred
   in ex buffer orelse ex chunks end;
 
 fun forall_string pred = not o exists_string (not o pred);
 
 fun last_string (Bytes {buffer, chunks, ...}) =
   (case buffer of
     s :: _ => Library.last_string s
   | [] =>
       (case chunks of
         s :: _ => Library.last_string s
       | [] => NONE));
 
 fun trim_line (bytes as Bytes {buffer, chunks, ...}) =
   let
     val is_line =
       (case last_string bytes of
         SOME s => Symbol.is_ascii_line_terminator s
       | NONE => false);
   in
     if is_line then
       let
         val (last_chunk, chunks') =
           (case chunks of
             [] => ("", [])
           | c :: cs => (c, cs));
         val trimed = Library.trim_line (last_chunk ^ compact buffer);
       in build (fold_rev add chunks' #> add trimed) end
     else bytes
   end;
 
 end;
 
 
 (* derived operations *)
 
 fun beginning n bytes =
   let
     val dots = " ...";
     val m = (String.maxSize - size dots) div chunk_size;
     val a = implode (take m (contents bytes));
     val b = String.substring (a, 0, Int.min (n, size a));
   in if size b < length bytes then b ^ dots else b end;
 
 fun append bytes1 bytes2 =  (*left-associative*)
   if is_empty bytes1 then bytes2
   else if is_empty bytes2 then bytes1
   else bytes1 |> fold add (contents bytes2);
 
 val appends = build o fold (fn b => fn a => append a b);
 
 val string = build o add;
 
 val newline = string "\n";
 
 val buffer = build o fold add o Buffer.contents;
 
 
 (* space_explode *)
 
 fun space_explode sep bytes =
   if is_empty bytes then []
   else if size sep <> 1 then [content bytes]
   else
     let
       val sep_char = String.sub (sep, 0);
 
       fun add_part s part =
         Buffer.add (Substring.string s) (the_default Buffer.empty part);
 
       fun explode head tail part res =
         if Substring.isEmpty head then
           (case tail of
             [] =>
               (case part of
                 NONE => rev res
               | SOME buf => rev (Buffer.content buf :: res))
           | chunk :: chunks => explode (Substring.full chunk) chunks part res)
         else
           (case Substring.fields (fn c => c = sep_char) head of
             [a] => explode Substring.empty tail (SOME (add_part a part)) res
           | a :: rest =>
               let
                 val (bs, c) = split_last rest;
                 val res' = res
                   |> cons (Buffer.content (add_part a part))
                   |> fold (cons o Substring.string) bs;
                 val part' = SOME (add_part c NONE);
               in explode Substring.empty tail part' res' end)
     in explode Substring.empty (contents bytes) NONE [] end;
 
 val split_lines = space_explode "\n";
 
 val trim_split_lines = trim_line #> split_lines #> map Library.trim_line;
 
 fun cat_lines lines = build (fold add (separate "\n" lines));
 
 
 (* IO *)
 
 fun read_block limit =
-  File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));
+  File_Stream.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));
 
 fun read_stream limit stream =
   let
     fun read bytes =
       (case read_block (limit - length bytes) stream of
         "" => bytes
       | s => read (add s bytes))
   in read empty end;
 
 fun write_stream stream bytes =
-  File.outputs stream (contents bytes);
+  File_Stream.outputs stream (contents bytes);
 
-fun read path = File.open_input (fn stream => read_stream ~1 stream) path;
+fun read path = File_Stream.open_input (fn stream => read_stream ~1 stream) path;
 
-fun write path bytes = File.open_output (fn stream => write_stream stream bytes) path;
+fun write path bytes = File_Stream.open_output (fn stream => write_stream stream bytes) path;
 
 
 (* ML pretty printing *)
 
 val _ =
   ML_system_pp (fn _ => fn _ => fn bytes =>
     PolyML.PrettyString ("Bytes {length = " ^ string_of_int (length bytes) ^ "}"))
 
 end;
diff --git a/src/Pure/General/file.ML b/src/Pure/General/file.ML
--- a/src/Pure/General/file.ML
+++ b/src/Pure/General/file.ML
@@ -1,184 +1,123 @@
 (*  Title:      Pure/General/file.ML
     Author:     Makarius
 
 File-system operations.
 *)
 
 signature FILE =
 sig
   val standard_path: Path.T -> string
   val platform_path: Path.T -> string
   val bash_path: Path.T -> string
   val bash_paths: Path.T list -> string
   val bash_platform_path: Path.T -> string
   val absolute_path: Path.T -> Path.T
   val full_path: Path.T -> Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val exists: Path.T -> bool
   val rm: Path.T -> unit
   val is_dir: Path.T -> bool
   val is_file: Path.T -> bool
   val check_dir: Path.T -> Path.T
   val check_file: Path.T -> Path.T
-  val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
-  val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a
-  val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a
-  val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a
   val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val read_dir: Path.T -> string list
-  val input: BinIO.instream -> string
-  val input_size: int -> BinIO.instream -> string
-  val input_all: BinIO.instream -> string
-  val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
+  val read: Path.T -> string
   val read_lines: Path.T -> string list
-  val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
-  val output: BinIO.outstream -> string -> unit
-  val outputs: BinIO.outstream -> string list -> unit
   val write_list: Path.T -> string list -> unit
   val append_list: Path.T -> string list -> unit
-  val write_buffer: Path.T -> Buffer.T -> unit
   val eq: Path.T * Path.T -> bool
 end;
 
 structure File: FILE =
 struct
 
 (* system path representations *)
 
 val standard_path = Path.implode o Path.expand;
 val platform_path = ML_System.platform_path o standard_path;
 
 val bash_path = Bash.string o standard_path;
 val bash_paths = Bash.strings o map standard_path;
 
 val bash_platform_path = Bash.string o platform_path;
 
 
 (* full_path *)
 
 val absolute_path =
   Path.expand #> (fn path =>
     if Path.is_absolute path then path
     else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path);
 
 fun full_path dir path =
   let
     val path' = Path.expand path;
     val _ = Path.is_current path' andalso error "Bad file specification";
   in absolute_path (dir + path') end;
 
 
 (* tmp_path *)
 
 fun tmp_path path = Path.variable "ISABELLE_TMP" + Path.base path;
 
 
 (* directory entries *)
 
 val exists = can OS.FileSys.modTime o platform_path;
 
 val rm = OS.FileSys.remove o platform_path;
 
 fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path));
 fun is_dir path = exists path andalso test_dir path;
 fun is_file path = exists path andalso not (test_dir path);
 
 fun check_dir path =
   if is_dir path then path
   else error ("No such directory: " ^ Path.print (Path.expand path));
 
 fun check_file path =
   if is_file path then path
   else error ("No such file: " ^ Path.print (Path.expand path));
 
 
-(* open streams *)
-
-local
-
-fun with_file open_file close_file f =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
-    let
-      val file = open_file path;
-      val result = Exn.capture (restore_attributes f) file;
-    in close_file file; Exn.release result end);
-
-in
-
-fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
-fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path;
-fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path;
-fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path;
-
-end;
-
-
 (* directory content *)
 
 fun fold_dir f path a =
-  check_dir path |> open_dir (fn stream =>
+  check_dir path |> File_Stream.open_dir (fn stream =>
     let
       fun read x =
         (case OS.FileSys.readDir stream of
           NONE => x
         | SOME entry => read (f entry x));
     in read a end);
 
 fun read_dir path = sort_strings (fold_dir cons path []);
 
 
-(* input *)
-
-val input = Byte.bytesToString o BinIO.input;
-fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n));
-val input_all = Byte.bytesToString o BinIO.inputAll;
+(* read *)
 
-(*
-  scalable iterator:
-  . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
-  . optional terminator at end-of-input
-*)
-fun fold_lines f path a = open_input (fn file =>
-  let
-    fun read buf x =
-      (case input file of
-        "" => (case Buffer.content buf of "" => x | line => f line x)
-      | input =>
-          (case String.fields (fn c => c = #"\n") input of
-            [rest] => read (Buffer.add rest buf) x
-          | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x)))
-    and read_more [rest] x = read (Buffer.add rest Buffer.empty) x
-      | read_more (line :: more) x = read_more more (f line x);
-  in read Buffer.empty a end) path;
+val read = File_Stream.open_input File_Stream.input_all;
 
-fun read_lines path = rev (fold_lines cons path []);
-
-val read = open_input input_all;
+val read_lines = Bytes.read #> Bytes.trim_split_lines;
 
 
-(* output *)
+(* write *)
 
-fun output file txt = BinIO.output (file, Byte.stringToBytes txt);
-val outputs = List.app o output;
-
-fun output_list txts file = List.app (output file) txts;
-fun write_list path txts = open_output (output_list txts) path;
-fun append_list path txts = open_append (output_list txts) path;
+fun write_list path ss = File_Stream.open_output (fn stream => File_Stream.outputs stream ss) path;
+fun append_list path ss = File_Stream.open_append (fn stream => File_Stream.outputs stream ss) path;
 
 fun write path txt = write_list path [txt];
 fun append path txt = append_list path [txt];
 
-fun write_buffer path buf =
-  open_output (fn file => List.app (output file) (Buffer.contents buf)) path;
-
 
 (* eq *)
 
 fun eq paths =
   (case try (apply2 (OS.FileSys.fileId o platform_path)) paths of
     SOME ids => is_equal (OS.FileSys.compare ids)
   | NONE => false);
 
 end;
diff --git a/src/Pure/General/file_stream.ML b/src/Pure/General/file_stream.ML
new file mode 100644
--- /dev/null
+++ b/src/Pure/General/file_stream.ML
@@ -0,0 +1,58 @@
+(*  Title:      Pure/General/file_stream.ML
+    Author:     Makarius
+
+File-system stream operations.
+*)
+
+signature FILE_STREAM =
+sig
+  val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
+  val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a
+  val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a
+  val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a
+  val input: BinIO.instream -> string
+  val input_size: int -> BinIO.instream -> string
+  val input_all: BinIO.instream -> string
+  val output: BinIO.outstream -> string -> unit
+  val outputs: BinIO.outstream -> string list -> unit
+end;
+
+structure File_Stream: FILE_STREAM =
+struct
+
+(* open streams *)
+
+local
+
+val platform_path = ML_System.platform_path o Path.implode o Path.expand;
+
+fun with_file open_file close_file f =
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
+    let
+      val file = open_file path;
+      val result = Exn.capture (restore_attributes f) file;
+    in close_file file; Exn.release result end);
+
+in
+
+fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
+fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path;
+fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path;
+fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path;
+
+end;
+
+
+(* input *)
+
+val input = Byte.bytesToString o BinIO.input;
+fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n));
+val input_all = Byte.bytesToString o BinIO.inputAll;
+
+
+(* output *)
+
+fun output file txt = BinIO.output (file, Byte.stringToBytes txt);
+val outputs = List.app o output;
+
+end;
diff --git a/src/Pure/PIDE/byte_message.ML b/src/Pure/PIDE/byte_message.ML
--- a/src/Pure/PIDE/byte_message.ML
+++ b/src/Pure/PIDE/byte_message.ML
@@ -1,127 +1,128 @@
 (*  Title:      Pure/General/byte_message.ML
     Author:     Makarius
 
 Byte-oriented messages.
 *)
 
 signature BYTE_MESSAGE =
 sig
   val write: BinIO.outstream -> Bytes.T list -> unit
   val write_yxml: BinIO.outstream -> XML.tree -> unit
   val flush: BinIO.outstream -> unit
   val write_line: BinIO.outstream -> Bytes.T -> unit
   val read: BinIO.instream -> int -> Bytes.T
   val read_block: BinIO.instream -> int -> Bytes.T option * int
   val read_line: BinIO.instream -> Bytes.T option
   val write_message: BinIO.outstream -> Bytes.T list -> unit
   val write_message_string: BinIO.outstream -> string list -> unit
   val write_message_yxml: BinIO.outstream -> XML.body list -> unit
   val read_message: BinIO.instream -> Bytes.T list option
   val read_message_string: BinIO.instream -> string list option
   val write_line_message: BinIO.outstream -> Bytes.T -> unit
   val read_line_message: BinIO.instream -> Bytes.T option
 end;
 
 structure Byte_Message: BYTE_MESSAGE =
 struct
 
 (* output operations *)
 
 val write = List.app o Bytes.write_stream;
 
-fun write_yxml stream tree = YXML.traverse (fn s => fn () => File.output stream s) tree ();
+fun write_yxml stream tree =
+  YXML.traverse (fn s => fn () => File_Stream.output stream s) tree ();
 
 fun flush stream = ignore (try BinIO.flushOut stream);
 
 fun write_line stream bs = (write stream [bs, Bytes.newline]; flush stream);
 
 
 (* input operations *)
 
 fun read stream n = Bytes.read_stream n stream;
 
 fun read_block stream n =
   let
     val msg = read stream n;
     val len = Bytes.length msg;
   in (if len = n then SOME msg else NONE, len) end;
 
 fun read_line stream =
   let
     val result = SOME o Bytes.trim_line;
     fun read_body bs =
       (case BinIO.input1 stream of
         NONE => if Bytes.is_empty bs then NONE else result bs
       | SOME b =>
           (case Byte.byteToChar b of
             #"\n" => result bs
           | c => read_body (Bytes.add (str c) bs)));
   in read_body Bytes.empty end;
 
 
 (* messages with multiple chunks (arbitrary content) *)
 
 fun make_header ns =
   [Bytes.string (space_implode "," (map Value.print_int ns)), Bytes.newline];
 
 fun write_message stream chunks =
   (write stream (make_header (map Bytes.length chunks) @ chunks); flush stream);
 
 fun write_message_string stream =
   write_message stream o map Bytes.string;
 
 fun write_message_yxml stream chunks =
   (write stream (make_header (map YXML.body_size chunks));
    (List.app o List.app) (write_yxml stream) chunks;
    flush stream);
 
 fun parse_header line =
   map Value.parse_nat (space_explode "," line)
     handle Fail _ => error ("Malformed message header: " ^ quote line);
 
 fun read_chunk stream n =
   (case read_block stream n of
     (SOME chunk, _) => chunk
   | (NONE, len) =>
       error ("Malformed message chunk: unexpected EOF after " ^
         string_of_int len ^ " of " ^ string_of_int n ^ " bytes"));
 
 fun read_message stream =
   read_line stream |> Option.map (Bytes.content #> parse_header #> map (read_chunk stream));
 
 fun read_message_string stream =
   read_message stream |> (Option.map o map) Bytes.content;
 
 
 (* hybrid messages: line or length+block (with content restriction) *)
 
 (* line message format *)
 
 fun is_length msg =
   not (Bytes.is_empty msg) andalso Bytes.forall_string Symbol.is_ascii_digit msg;
 
 fun is_terminated msg =
   (case Bytes.last_string msg of
     NONE => false
   | SOME s => Symbol.is_ascii_line_terminator s);
 
 fun write_line_message stream msg =
   if is_length msg orelse is_terminated msg then
     error ("Bad content for line message:\n" ^ Bytes.beginning 100 msg)
   else
     let val n = Bytes.length msg in
       write stream
         ((if n > 100 orelse Bytes.exists_string (fn s => s = "\n") msg
           then make_header [n + 1] else []) @ [msg, Bytes.newline]);
       flush stream
     end;
 
 fun read_line_message stream =
   (case read_line stream of
     NONE => NONE
   | SOME line =>
       (case try (Value.parse_nat o Bytes.content) line of
         NONE => SOME line
       | SOME n => Option.map Bytes.trim_line (#1 (read_block stream n))));
 
 end;
diff --git a/src/Pure/PIDE/yxml.ML b/src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML
+++ b/src/Pure/PIDE/yxml.ML
@@ -1,175 +1,175 @@
 (*  Title:      Pure/PIDE/yxml.ML
     Author:     Makarius
 
 Efficient text representation of XML trees using extra characters X
 and Y -- no escaping, may nest marked text verbatim.  Suitable for
 direct inlining into plain text.
 
 Markup <elem att="val" ...>...body...</elem> is encoded as:
 
   X Y name Y att=val ... X
   ...
   body
   ...
   X Y X
 *)
 
 signature YXML =
 sig
   val X: Symbol.symbol
   val Y: Symbol.symbol
   val embed_controls: string -> string
   val detect: string -> bool
   val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
   val tree_size: XML.tree -> int
   val body_size: XML.body -> int
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val write_body: Path.T -> XML.body -> unit
   val output_markup: Markup.T -> string * string
   val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
   val content_of: string -> string
   val is_wellformed: string -> bool
 end;
 
 structure YXML: YXML =
 struct
 
 (** string representation **)
 
 (* idempotent recoding of certain low ASCII control characters *)
 
 fun pseudo_utf8 c =
   if Symbol.is_ascii_control c
   then chr 192 ^ chr (128 + ord c)
   else c;
 
 fun embed_controls str =
   if exists_string Symbol.is_ascii_control str
   then translate_string pseudo_utf8 str
   else str;
 
 
 (* markers *)
 
 val X_char = Char.chr 5;
 val Y_char = Char.chr 6;
 
 val X = String.str X_char;
 val Y = String.str Y_char;
 val XY = X ^ Y;
 val XYX = XY ^ X;
 
 fun detect s = Char.contains s X_char orelse Char.contains s Y_char;
 
 
 (* traverse *)
 
 fun traverse string =
   let
     fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
     fun tree (XML.Elem (markup as (name, atts), ts)) =
           if Markup.is_empty markup then fold tree ts
           else
             string XY #> string name #> fold attrib atts #> string X #>
             fold tree ts #>
             string XYX
       | tree (XML.Text s) = string s;
   in tree end;
 
 fun tree_size tree = traverse (Integer.add o size) tree 0;
 fun body_size body = fold (Integer.add o tree_size) body 0;
 
 
 (* output *)
 
 val string_of_body = Buffer.build_content o fold (traverse Buffer.add);
 val string_of = string_of_body o single;
 
 fun write_body path body =
-  path |> File.open_output (fn file =>
-    fold (traverse (fn s => fn () => File.output file s)) body ());
+  path |> File_Stream.open_output (fn file =>
+    fold (traverse (fn s => fn () => File_Stream.output file s)) body ());
 
 
 (* markup elements *)
 
 val Z = chr 0;
 val Z_text = [XML.Text Z];
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
 fun output_markup_elem markup =
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
   in ((bg1, bg2), en) end;
 
 
 
 (** efficient YXML parsing **)
 
 local
 
 (* splitting *)
 
 val split_string =
   Substring.full #>
   Substring.tokens (fn c => c = X_char) #>
   map (Substring.fields (fn c => c = Y_char) #> map Substring.string);
 
 
 (* structural errors *)
 
 fun err msg = raise Fail ("Malformed YXML: " ^ msg);
 fun err_attribute () = err "bad attribute";
 fun err_element () = err "bad element";
 fun err_unbalanced "" = err "unbalanced element"
   | err_unbalanced name = err ("unbalanced element " ^ quote name);
 
 
 (* stack operations *)
 
 fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
 
 fun push "" _ _ = err_element ()
   | push name atts pending = ((name, atts), []) :: pending;
 
 fun pop ((("", _), _) :: _) = err_unbalanced ""
   | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
 
 
 (* parsing *)
 
 fun parse_attrib s =
   (case first_field "=" s of
     NONE => err_attribute ()
   | SOME ("", _) => err_attribute ()
   | SOME att => att);
 
 fun parse_chunk ["", ""] = pop
   | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
   | parse_chunk txts = fold (add o XML.Text) txts;
 
 in
 
 fun parse_body source =
   (case fold parse_chunk (split_string source) [(("", []), [])] of
     [(("", _), result)] => rev result
   | ((name, _), _) :: _ => err_unbalanced name);
 
 fun parse source =
   (case parse_body source of
     [result] => result
   | [] => XML.Text ""
   | _ => err "multiple results");
 
 end;
 
 val content_of = parse_body #> XML.content_of;
 
 fun is_wellformed s = string_of_body (parse_body s) = s
   handle Fail _ => false;
 
 end;
diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML
+++ b/src/Pure/ROOT.ML
@@ -1,362 +1,363 @@
 (*  Title:      Pure/ROOT.ML
     Author:     Makarius
 
 Main entry point for the Isabelle/Pure bootstrap process.
 
 Note: When this file is open in the Prover IDE, the ML files of
 Isabelle/Pure can be explored interactively. This is a separate copy of
 Pure within Pure: it does not affect the running logic session.
 *)
 
 chapter "Isabelle/Pure bootstrap";
 
 ML_file "ML/ml_name_space.ML";
 
 
 section "Bootstrap phase 0: Poly/ML setup";
 
 ML_file "ML/ml_init.ML";
 ML_file "ML/ml_system.ML";
 
 ML_file "General/basics.ML";
 ML_file "General/symbol_explode.ML";
 
 ML_file "Concurrent/multithreading.ML";
 ML_file "Concurrent/unsynchronized.ML";
 ML_file "Concurrent/synchronized.ML";
 ML_file "Concurrent/counter.ML";
 
 ML_file "ML/ml_heap.ML";
 ML_file "ML/ml_print_depth0.ML";
 ML_file "ML/ml_pretty.ML";
 ML_file "ML/ml_compiler0.ML";
 
 
 section "Bootstrap phase 1: towards ML within position context";
 
 subsection "Library of general tools";
 
 ML_file "library.ML";
 ML_file "General/print_mode.ML";
 ML_file "General/alist.ML";
 ML_file "General/table.ML";
 
 ML_file "General/random.ML";
 ML_file "General/value.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
 ML_file "PIDE/markup.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
 ML_file "General/source.ML";
 ML_file "General/symbol.ML";
 ML_file "General/position.ML";
 ML_file "General/symbol_pos.ML";
 ML_file "General/input.ML";
 ML_file "General/comment.ML";
 ML_file "General/antiquote.ML";
 ML_file "ML/ml_lex.ML";
 ML_file "ML/ml_compiler1.ML";
 
 
 section "Bootstrap phase 2: towards ML within Isar context";
 
 subsection "Library of general tools";
 
 ML_file "General/integer.ML";
 ML_file "General/stack.ML";
 ML_file "General/queue.ML";
 ML_file "General/heap.ML";
 ML_file "General/same.ML";
 ML_file "General/ord_list.ML";
 ML_file "General/balanced_tree.ML";
 ML_file "General/linear_set.ML";
 ML_file "General/buffer.ML";
 ML_file "General/pretty.ML";
 ML_file "General/rat.ML";
 ML_file "PIDE/xml.ML";
 ML_file "General/path.ML";
 ML_file "General/url.ML";
 ML_file "System/bash.ML";
+ML_file "General/file_stream.ML";
+ML_file "General/bytes.ML";
 ML_file "General/file.ML";
-ML_file "General/bytes.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/seq.ML";
 ML_file "General/time.ML";
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";
 
 ML_file "PIDE/yxml.ML";
 ML_file "ML/ml_profiling.ML";
 ML_file "PIDE/byte_message.ML";
 ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document_id.ML";
 ML_file "General/socket_io.ML";
 
 ML_file "General/change_table.ML";
 ML_file "General/graph.ML";
 
 ML_file "System/options.ML";
 
 
 subsection "Fundamental structures";
 
 ML_file "name.ML";
 ML_file "term.ML";
 ML_file "context.ML";
 ML_file "config.ML";
 ML_file "context_position.ML";
 ML_file "soft_type_system.ML";
 
 
 subsection "Concurrency within the ML runtime";
 
 ML_file "ML/exn_properties.ML";
 ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
 ML_file "Concurrent/isabelle_thread.ML";
 ML_file "Concurrent/single_assignment.ML";
 
 ML_file "Concurrent/par_exn.ML";
 ML_file "Concurrent/task_queue.ML";
 ML_file "Concurrent/future.ML";
 ML_file "Concurrent/event_timer.ML";
 ML_file "Concurrent/timeout.ML";
 ML_file "Concurrent/lazy.ML";
 ML_file "Concurrent/par_list.ML";
 
 ML_file "Concurrent/mailbox.ML";
 ML_file "Concurrent/cache.ML";
 
 ML_file "PIDE/active.ML";
 ML_file "Thy/export.ML";
 
 
 subsection "Inner syntax";
 
 ML_file "Syntax/type_annotation.ML";
 ML_file "Syntax/term_position.ML";
 ML_file "Syntax/lexicon.ML";
 ML_file "Syntax/ast.ML";
 ML_file "Syntax/syntax_ext.ML";
 ML_file "Syntax/parser.ML";
 ML_file "Syntax/syntax_trans.ML";
 ML_file "Syntax/mixfix.ML";
 ML_file "Syntax/printer.ML";
 ML_file "Syntax/syntax.ML";
 
 
 subsection "Core of tactical proof system";
 
 ML_file "term_ord.ML";
 ML_file "term_items.ML";
 ML_file "term_subst.ML";
 ML_file "General/completion.ML";
 ML_file "General/name_space.ML";
 ML_file "sorts.ML";
 ML_file "type.ML";
 ML_file "logic.ML";
 ML_file "Syntax/simple_syntax.ML";
 ML_file "net.ML";
 ML_file "item_net.ML";
 ML_file "envir.ML";
 ML_file "consts.ML";
 ML_file "term_xml.ML";
 ML_file "primitive_defs.ML";
 ML_file "sign.ML";
 ML_file "defs.ML";
 ML_file "term_sharing.ML";
 ML_file "pattern.ML";
 ML_file "unify.ML";
 ML_file "theory.ML";
 ML_file "proofterm.ML";
 ML_file "thm.ML";
 ML_file "cterm_items.ML";
 ML_file "more_pattern.ML";
 ML_file "more_unify.ML";
 ML_file "more_thm.ML";
 
 ML_file "facts.ML";
 ML_file "thm_name.ML";
 ML_file "global_theory.ML";
 ML_file "pure_thy.ML";
 ML_file "drule.ML";
 ML_file "morphism.ML";
 ML_file "variable.ML";
 ML_file "conv.ML";
 ML_file "goal_display.ML";
 ML_file "tactical.ML";
 ML_file "search.ML";
 ML_file "tactic.ML";
 ML_file "raw_simplifier.ML";
 ML_file "conjunction.ML";
 ML_file "assumption.ML";
 
 
 subsection "Isar -- Intelligible Semi-Automated Reasoning";
 
 (*ML support and global execution*)
 ML_file "ML/ml_syntax.ML";
 ML_file "ML/ml_env.ML";
 ML_file "ML/ml_options.ML";
 ML_file "ML/ml_print_depth.ML";
 ML_file_no_debug "Isar/runtime.ML";
 ML_file "PIDE/execution.ML";
 ML_file "ML/ml_compiler.ML";
 
 ML_file "skip_proof.ML";
 ML_file "goal.ML";
 
 (*outer syntax*)
 ML_file "Isar/keyword.ML";
 ML_file "Isar/token.ML";
 ML_file "Isar/parse.ML";
 ML_file "Thy/document_source.ML";
 ML_file "Thy/thy_header.ML";
 ML_file "Thy/document_marker.ML";
 
 (*proof context*)
 ML_file "Isar/object_logic.ML";
 ML_file "Isar/rule_cases.ML";
 ML_file "Isar/auto_bind.ML";
 ML_file "type_infer.ML";
 ML_file "Syntax/local_syntax.ML";
 ML_file "Isar/proof_context.ML";
 ML_file "type_infer_context.ML";
 ML_file "Syntax/syntax_phases.ML";
 ML_file "Isar/args.ML";
 
 (*theory specifications*)
 ML_file "Isar/local_defs.ML";
 ML_file "Isar/local_theory.ML";
 ML_file "Isar/entity.ML";
 ML_file "PIDE/command_span.ML";
 ML_file "Thy/thy_element.ML";
 ML_file "Thy/markdown.ML";
 ML_file "Thy/latex.ML";
 
 (*ML with context and antiquotations*)
 ML_file "ML/ml_context.ML";
 ML_file "ML/ml_antiquotation.ML";
 ML_file "ML/ml_compiler2.ML";
 ML_file "ML/ml_antiquotations.ML";
 
 
 section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
 
 (*basic proof engine*)
 ML_file "par_tactical.ML";
 ML_file "context_tactic.ML";
 ML_file "Isar/proof_display.ML";
 ML_file "Isar/attrib.ML";
 ML_file "Isar/context_rules.ML";
 ML_file "Isar/method.ML";
 ML_file "Isar/proof.ML";
 ML_file "Isar/element.ML";
 ML_file "Isar/obtain.ML";
 ML_file "Isar/subgoal.ML";
 ML_file "Isar/calculation.ML";
 
 (*local theories and targets*)
 ML_file "Isar/locale.ML";
 ML_file "Isar/generic_target.ML";
 ML_file "Isar/bundle.ML";
 ML_file "Isar/overloading.ML";
 ML_file "axclass.ML";
 ML_file "Isar/class.ML";
 ML_file "Isar/named_target.ML";
 ML_file "Isar/expression.ML";
 ML_file "Isar/interpretation.ML";
 ML_file "Isar/class_declaration.ML";
 ML_file "Isar/target_context.ML";
 ML_file "Isar/experiment.ML";
 ML_file "simplifier.ML";
 ML_file "Tools/plugin.ML";
 
 (*executable theory content*)
 ML_file "Isar/code.ML";
 
 (*specifications*)
 ML_file "Isar/spec_rules.ML";
 ML_file "Isar/specification.ML";
 ML_file "Isar/parse_spec.ML";
 ML_file "Isar/typedecl.ML";
 
 (*toplevel transactions*)
 ML_file "Isar/proof_node.ML";
 ML_file "Isar/toplevel.ML";
 
 (*proof term operations*)
 ML_file "Proof/proof_rewrite_rules.ML";
 ML_file "Proof/proof_syntax.ML";
 ML_file "Proof/proof_checker.ML";
 ML_file "Proof/extraction.ML";
 
 (*Isabelle system*)
 ML_file "PIDE/protocol_command.ML";
 ML_file "System/scala.ML";
 ML_file "System/process_result.ML";
 ML_file "System/isabelle_system.ML";
 
 
 (*theory documents*)
 ML_file "Thy/term_style.ML";
 ML_file "Isar/outer_syntax.ML";
 ML_file "Thy/document_antiquotation.ML";
 ML_file "Thy/document_output.ML";
 ML_file "Thy/document_antiquotations.ML";
 ML_file "General/graph_display.ML";
 ML_file "pure_syn.ML";
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
 ML_file "PIDE/resources.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "thm_deps.ML";
 ML_file "Thy/export_theory.ML";
 ML_file "Thy/sessions.ML";
 ML_file "PIDE/session.ML";
 ML_file "PIDE/document.ML";
 
 (*ML add-ons*)
 ML_file "ML/ml_pp.ML";
 ML_file "ML/ml_thms.ML";
 ML_file "ML/ml_instantiate.ML";
 ML_file "ML/ml_file.ML";
 ML_file "ML/ml_pid.ML";
 
 (*theory and proof operations*)
 ML_file "Isar/isar_cmd.ML";
 
 
 subsection "Isabelle/Isar system";
 
 ML_file "System/command_line.ML";
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
 ML_file "System/scala_compiler.ML";
 ML_file "System/isabelle_tool.ML";
 ML_file "Thy/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";
 
 
 subsection "Miscellaneous tools and packages for Pure Isabelle";
 
 ML_file "Tools/build.ML";
 ML_file "Tools/named_thms.ML";
 ML_file "Tools/print_operation.ML";
 ML_file "Tools/rail.ML";
 ML_file "Tools/rule_insts.ML";
 ML_file "Tools/thy_deps.ML";
 ML_file "Tools/class_deps.ML";
 ML_file "Tools/find_theorems.ML";
 ML_file "Tools/find_consts.ML";
 ML_file "Tools/simplifier_trace.ML";
 ML_file_no_debug "Tools/debugger.ML";
 ML_file "Tools/named_theorems.ML";
 ML_file "Tools/doc.ML";
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML"
diff --git a/src/Tools/cache_io.ML b/src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML
+++ b/src/Tools/cache_io.ML
@@ -1,126 +1,126 @@
 (*  Title:      Tools/cache_io.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Cache for output of external processes.
 *)
 
 signature CACHE_IO =
 sig
   (*IO wrapper*)
   type result = {
     output: string list,
     redirected_output: string list,
     return_code: int}
   val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> result
   val run: (Path.T -> Path.T -> string) -> string -> result
 
   (*cache*)
   type cache
   val unsynchronized_init: Path.T -> cache
   val cache_path_of: cache -> Path.T
   val lookup: cache -> string -> result option * string
   val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result
   val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
 end
 
 structure Cache_IO : CACHE_IO =
 struct
 
 (* IO wrapper *)
 
 val cache_io_prefix = "cache-io-"
 
 type result = {
   output: string list,
   redirected_output: string list,
   return_code: int}
 
 fun raw_run make_cmd str in_path out_path =
   let
     val _ = File.write in_path str
     val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
-    val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
+    val out1 = the_default [] (try File.read_lines out_path)
   in {output = split_lines out2, redirected_output = out1, return_code = rc} end
 
 fun run make_cmd str =
   Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path =>
     Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path =>
       raw_run make_cmd str in_path out_path))
 
 
 (* cache *)
 
 abstype cache = Cache of {
   path: Path.T,
   table: (int * (int * int * int) Symtab.table) Synchronized.var }
 with
 
 fun cache_path_of (Cache {path, ...}) = path
 
 fun unsynchronized_init cache_path =
   let
     val table =
       if File.exists cache_path then
         let
           fun err () = error ("Cache IO: corrupted cache file: " ^ File.bash_path cache_path)
 
           fun int_of_string s =
             (case read_int (raw_explode s) of
               (i, []) => i
             | _ => err ())
 
           fun split line =
             (case space_explode " " line of
               [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
             | _ => err ())
 
           fun parse line ((i, l), tab) =
             if i = l
             then
               let val (key, l1, l2) = split line
               in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
             else ((i+1, l), tab)
-        in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
+        in apfst fst (fold parse (File.read_lines cache_path) ((1, 1), Symtab.empty)) end
       else (1, Symtab.empty)
   in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end
 
 fun lookup (Cache {path = cache_path, table}) str =
   let val key = SHA1.rep (SHA1.digest str)
   in
     Synchronized.change_result table (fn tab =>
       (case Symtab.lookup (snd tab) key of
         NONE => ((NONE, key), tab)
       | SOME (p, len1, len2) =>
           let
             fun load line (i, xsp) =
               if i < p then (i+1, xsp)
               else if i < p + len1 then (i+1, apfst (cons line) xsp)
               else if i < p + len2 then (i+1, apsnd (cons line) xsp)
               else (i, xsp)
             val (out, err) =
-              apply2 rev (snd (File.fold_lines load cache_path (1, ([], []))))
+              apply2 rev (snd (fold load (File.read_lines cache_path) (1, ([], []))))
           in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
   end
 
 fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =
   let
     val {output = err, redirected_output=out, return_code} = run make_cmd str
     val (l1, l2) = apply2 length (out, err)
     val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
     val lines = map (suffix "\n") (header :: out @ err)
 
     val _ = Synchronized.change table (fn (p, tab) =>
       if Symtab.defined tab key then (p, tab)
       else
         let val _ = File.append_list cache_path lines
         in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
   in {output = err, redirected_output = out, return_code = return_code} end
 
 fun run_cached cache make_cmd str =
   (case lookup cache str of
     (NONE, key) => run_and_cache cache key make_cmd str
   | (SOME output, _) => output)
 
 end
 
 end