diff -r e9ab4ad7bd15 -r 23307fd33906 src/Doc/Tutorial/Misc/Tree.thy
--- a/src/Doc/Tutorial/Misc/Tree.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Misc/Tree.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -2,9 +2,9 @@
 theory Tree imports Main begin
 (*>*)
 
-text{*\noindent
+text\<open>\noindent
 Define the datatype of \rmindex{binary trees}:
-*}
+\<close>
 
 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"(*<*)
 
@@ -12,10 +12,10 @@
 "mirror Tip = Tip" |
 "mirror (Node l x r) = Node (mirror r) x (mirror l)"(*>*)
 
-text{*\noindent
+text\<open>\noindent
 Define a function @{term"mirror"} that mirrors a binary tree
 by swapping subtrees recursively. Prove
-*}
+\<close>
 
 lemma mirror_mirror: "mirror(mirror t) = t"
 (*<*)
@@ -27,10 +27,10 @@
 "flatten (Node l x r) = flatten l @ [x] @ flatten r"
 (*>*)
 
-text{*\noindent
+text\<open>\noindent
 Define a function @{term"flatten"} that flattens a tree into a list
 by traversing it in infix order. Prove
-*}
+\<close>
 
 lemma "flatten(mirror t) = rev(flatten t)"
 (*<*)