diff -r 21c2b1f691d1 -r 0d399131008f src/Tools/SML/Examples.thy
--- a/src/Tools/SML/Examples.thy	Mon Nov 30 13:16:12 2015 +0100
+++ b/src/Tools/SML/Examples.thy	Mon Nov 30 14:24:51 2015 +0100
@@ -9,12 +9,12 @@
 begin
 
 text \<open>
-  Isabelle/ML is a somewhat augmented version of Standard ML, with
-  various add-ons that are indispensable for Isabelle development, but
-  may cause conflicts with independent projects in plain Standard ML.
+  Isabelle/ML is a somewhat augmented version of Standard ML, with various
+  add-ons that are indispensable for Isabelle development, but may cause
+  conflicts with independent projects in plain Standard ML.
 
-  The Isabelle/Isar command 'SML_file' supports official Standard ML
-  within the Isabelle environment, with full support in the Prover IDE
+  The Isabelle/Isar command \<^theory_text>\<open>SML_file\<close> supports official Standard ML within
+  the Isabelle environment, with full support in the Prover IDE
   (Isabelle/jEdit).
 
   Here is a very basic example that defines the factorial function and
@@ -24,10 +24,10 @@
 SML_file "factorial.sml"
 
 text \<open>
-  The subsequent example illustrates the use of multiple 'SML_file'
-  commands to build larger Standard ML projects.  The toplevel SML
-  environment is enriched cumulatively within the theory context of
-  Isabelle --- independently of the Isabelle/ML environment.
+  The subsequent example illustrates the use of multiple \<^theory_text>\<open>SML_file\<close> commands
+  to build larger Standard ML projects. The toplevel SML environment is
+  enriched cumulatively within the theory context of Isabelle ---
+  independently of the Isabelle/ML environment.
 \<close>
 
 SML_file "Example.sig"
@@ -36,17 +36,17 @@
 
 text \<open>
   Isabelle/ML and SML share a common run-time system, but the static
-  environments are separate.  It is possible to exchange toplevel bindings
-  via separate commands like this.
+  environments are separate. It is possible to exchange toplevel bindings via
+  separate commands like this.
 \<close>
 
-SML_export \<open>val f = factorial\<close>  -- \<open>re-use factorial from SML environment\<close>
+SML_export \<open>val f = factorial\<close>  \<comment> \<open>re-use factorial from SML environment\<close>
 ML \<open>f 42\<close>
 
 SML_import \<open>val println = Output.writeln\<close>
-  -- \<open>re-use Isabelle/ML channel for SML\<close>
+  \<comment> \<open>re-use Isabelle/ML channel for SML\<close>
 
 SML_import \<open>val par_map = Par_List.map\<close>
-  -- \<open>re-use Isabelle/ML parallel list combinator for SML\<close>
+  \<comment> \<open>re-use Isabelle/ML parallel list combinator for SML\<close>
 
 end