diff -r 54a3db2ed201 -r 903bb1495239 src/HOL/Library/Debug.thy
--- a/src/HOL/Library/Debug.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Debug.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -1,6 +1,6 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-section {* Debugging facilities for code generated towards Isabelle/ML *}
+section \<open>Debugging facilities for code generated towards Isabelle/ML\<close>
 
 theory Debug
 imports Main
@@ -31,7 +31,7 @@
 
 code_printing
   constant trace \<rightharpoonup> (Eval) "Output.tracing"
-| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- {* note indirection via antiquotation *}
+| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
 | constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
 
 code_reserved Eval Output Timing