# HG changeset patch
# User wenzelm
# Date 1696785461 -7200
# Node ID 39498d504f4314aa73588e1a5f5d1a3009ab7715
# Parent  45ff003d337c802d9e90803b1a7db96b895d759f
misc tuning;

diff -r 45ff003d337c -r 39498d504f43 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Sun Oct 08 19:05:35 2023 +0200
+++ b/src/Doc/Implementation/ML.thy	Sun Oct 08 19:17:41 2023 +0200
@@ -1106,8 +1106,9 @@
   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.
+  this is not strictly 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.\
@@ -1120,8 +1121,8 @@
 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
-  special exceptions user code, satisfying the predicate
+  Isabelle/ML infrastructure may signal various exceptional situations by
+  raising special exceptions user code, satisfying the predicate
   \<^ML>\<open>Exn.is_interrupt\<close>.
 
   This is the one and only way that physical events can intrude an Isabelle/ML
@@ -1159,10 +1160,6 @@
   @{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
@@ -1200,6 +1197,10 @@
   @{ML_antiquotation_def "undefined"} & : & \<open>ML_antiquotation\<close> \\
   \end{matharray}
 
+  \<^rail>\<open>
+    (@@{ML_antiquotation try} | @@{ML_antiquotation can}) embedded
+  \<close>
+
   \<^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.
@@ -1238,7 +1239,7 @@
   instead:
 \<close>
 
-ML \<open>fun undefined _ = \<^undefined>\<close>
+ML \<open>fun undefined _ = @{undefined}\<close>
 
 text \<open>
   \<^medskip>
@@ -1249,8 +1250,9 @@
 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.
+  \<^medskip>
+  Semantically, all forms are equivalent to a function definition without any
+  clauses, but that is syntactically not allowed in ML.
 \<close>