diff -r e9ab4ad7bd15 -r 23307fd33906 src/Doc/Tutorial/Recdef/Nested0.thy
--- a/src/Doc/Tutorial/Recdef/Nested0.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Recdef/Nested0.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -2,14 +2,14 @@
 theory Nested0 imports Main begin
 (*>*)
 
-text{*
+text\<open>
 \index{datatypes!nested}%
 In \S\ref{sec:nested-datatype} we defined the datatype of terms
-*}
+\<close>
 
 datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list"
 
-text{*\noindent
+text\<open>\noindent
 and closed with the observation that the associated schema for the definition
 of primitive recursive functions leads to overly verbose definitions. Moreover,
 if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
@@ -18,7 +18,7 @@
 We will now show you how \isacommand{recdef} can simplify
 definitions and proofs about nested recursive datatypes. As an example we
 choose exercise~\ref{ex:trev-trev}:
-*}
+\<close>
 
 consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term"
 (*<*)end(*>*)