diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Discrete.thy
--- a/src/HOL/HOLCF/Discrete.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Discrete.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow
 *)
 
-section {* Discrete cpo types *}
+section \<open>Discrete cpo types\<close>
 
 theory Discrete
 imports Cont
@@ -10,7 +10,7 @@
 
 datatype 'a discr = Discr "'a :: type"
 
-subsection {* Discrete cpo class instance *}
+subsection \<open>Discrete cpo class instance\<close>
 
 instantiation discr :: (type) discrete_cpo
 begin
@@ -23,7 +23,7 @@
 
 end
 
-subsection {* \emph{undiscr} *}
+subsection \<open>\emph{undiscr}\<close>
 
 definition
   undiscr :: "('a::type)discr => 'a" where