diff -r c38d8f139bbc -r 4257a7f2bf39 src/Tools/SML/Examples.thy
--- a/src/Tools/SML/Examples.thy	Tue Oct 07 21:01:31 2014 +0200
+++ b/src/Tools/SML/Examples.thy	Tue Oct 07 21:11:18 2014 +0200
@@ -2,13 +2,13 @@
     Author:     Makarius
 *)
 
-header {* Standard ML within the Isabelle environment *}
+header \<open>Standard ML within the Isabelle environment\<close>
 
 theory Examples
 imports Pure
 begin
 
-text {*
+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.
@@ -19,34 +19,34 @@
 
   Here is a very basic example that defines the factorial function and
   evaluates it for some arguments.
-*}
+\<close>
 
 SML_file "factorial.sml"
 
-text {*
+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.
-*}
+\<close>
 
 SML_file "Example.sig"
 SML_file "Example.sml"
 
 
-text {*
+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.
-*}
+\<close>
 
-SML_export {* val f = factorial *}  -- {* re-use factorial from SML environment *}
-ML {* f 42 *}
+SML_export \<open>val f = factorial\<close>  -- \<open>re-use factorial from SML environment\<close>
+ML \<open>f 42\<close>
 
-SML_import {* val println = Output.writeln *}
-  -- {* re-use Isabelle/ML channel for SML *}
+SML_import \<open>val println = Output.writeln\<close>
+  -- \<open>re-use Isabelle/ML channel for SML\<close>
 
-SML_import {* val par_map = Par_List.map *}
-  -- {* re-use Isabelle/ML parallel list combinator for SML *}
+SML_import \<open>val par_map = Par_List.map\<close>
+  -- \<open>re-use Isabelle/ML parallel list combinator for SML\<close>
 
 end