--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Tue May 14 11:10:53 2019 +0200
@@ -57,8 +57,8 @@
 
   \begin{isabelle}
   @{text "rule ::= 
-  \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow> 
-  \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^raw:}}_{\text{\rm recursive premises}}$> 
+  \<And>xs. \<^latex>\<open>$\\underbrace{\\mbox{\<close>As\<^latex>\<open>}}_{\\text{\\makebox[0mm]{\\rm non-recursive premises}}}$\<close> \<Longrightarrow> 
+  \<^latex>\<open>$\\underbrace{\\mbox{\<close>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^latex>\<open>}}_{\\text{\\rm recursive premises}}$>\<close> 
   \<Longrightarrow> pred ts"}
   \end{isabelle}