diff -r cf7f3465eaf1 -r 240563fbf41d src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/Sequents/Sequents.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-section {* Parsing and pretty-printing of sequences *}
+section \<open>Parsing and pretty-printing of sequences\<close>
 
 theory Sequents
 imports Pure
@@ -17,7 +17,7 @@
 typedecl o
 
 
-subsection {* Sequences *}
+subsection \<open>Sequences\<close>
 
 typedecl
  seq'
@@ -27,7 +27,7 @@
  Seq1'         :: "o=>seq'"
 
 
-subsection {* Concrete syntax *}
+subsection \<open>Concrete syntax\<close>
 
 nonterminal seq and seqobj and seqcont
 
@@ -56,7 +56,7 @@
   (*Constant to allow definitions of SEQUENCES of formulas*)
   "_Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
 
-ML {*
+ML \<open>
 
 (* parse translation for sequences *)
 
@@ -139,12 +139,12 @@
 (** for the <<...>> notation **)
 
 fun side_tr [s1] = seq_tr s1;
-*}
+\<close>
 
-parse_translation {* [(@{syntax_const "_Side"}, K side_tr)] *}
+parse_translation \<open>[(@{syntax_const "_Side"}, K side_tr)]\<close>
 
 
-subsection {* Proof tools *}
+subsection \<open>Proof tools\<close>
 
 ML_file "prover.ML"