diff -r e85099ac4c6c -r 692b62426677 thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Wed Sep 06 00:52:08 2017 +0100
+++ b/thys/Journal/Paper.thy	Fri Sep 22 12:25:25 2017 +0100
@@ -16,7 +16,7 @@
 declare [[show_question_marks = false]]
 
 syntax (latex output)
-  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ \<^raw:\mbox{\boldmath$\mid$}> _})")
+  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ \<^latex>\<open>\\mbox{\\boldmath$\\mid$}\<close> _})")
   "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ |e _})")
 
 syntax
@@ -38,8 +38,8 @@
 
 
 notation (latex output)
-  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
-  Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and  
+  If  ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and
+  Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and  
 
   ZERO ("\<^bold>0" 81) and 
   ONE ("\<^bold>1" 81) and 
@@ -82,15 +82,15 @@
   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
   slexer ("lexer\<^sup>+" 1000) and
 
-  at ("_\<^raw:\mbox{$\downharpoonleft$}>\<^bsub>_\<^esub>") and
+  at ("_\<^latex>\<open>\\mbox{$\\downharpoonleft$}\<close>\<^bsub>_\<^esub>") and
   lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and
   PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and
   PosOrd_ex ("_ \<prec> _" [77,77] 77) and
-  PosOrd_ex_eq ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and
+  PosOrd_ex_eq ("_ \<^latex>\<open>\\mbox{$\\preccurlyeq$}\<close> _" [77,77] 77) and
   pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and
-  nprec ("_ \<^raw:\mbox{$\not\prec$}> _" [77,77] 77) and
+  nprec ("_ \<^latex>\<open>\\mbox{$\\not\\prec$}\<close> _" [77,77] 77) and
 
-  DUMMY ("\<^raw:\underline{\hspace{2mm}}>")
+  DUMMY ("\<^latex>\<open>\\underline{\\hspace{2mm}}\<close>")
 
 
 definition