diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Nitpick_Examples/Special_Nits.thy
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Thu May 26 17:51:22 2016 +0200
@@ -5,7 +5,7 @@
 Examples featuring Nitpick's "specialize" optimization.
 *)
 
-section {* Examples Featuring Nitpick's \textit{specialize} Optimization *}
+section \<open>Examples Featuring Nitpick's \textit{specialize} Optimization\<close>
 
 theory Special_Nits
 imports Main