diff -r af069653f1d7 -r a04bf731ceb6 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Mon Sep 04 20:07:55 2006 +0200
@@ -150,10 +150,10 @@
 
   The operational part is represented as the sequential union of a
   list of partial functions, which are tried in turn until the first
-  one succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|).  This acts
-  like an outer case-expression for various alternative state
-  transitions.  For example, \isakeyword{qed} acts differently for a
-  local proofs vs.\ the global ending of the main proof.
+  one succeeds.  This acts like an outer case-expression for various
+  alternative state transitions.  For example, \isakeyword{qed} acts
+  differently for a local proofs vs.\ the global ending of the main
+  proof.
 
   Toplevel transitions are composed via transition transformers.
   Internally, Isar commands are put together from an empty transition
@@ -274,9 +274,9 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The {\ML} toplevel provides a read-compile-eval-print loop for
-  {\ML} values, types, structures, and functors.  {\ML} declarations
-  operate on the global system state, which consists of the compiler
+The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
+  values, types, structures, and functors.  {\ML} declarations operate
+  on the global system state, which consists of the compiler
   environment plus the values of {\ML} reference variables.  There is
   no clean way to undo {\ML} declarations, except for reverting to a
   previously saved state of the whole Isabelle process.  {\ML} input