diff -r c09598a97436 -r d8d85a8172b5 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/BNF_Def.thy	Sat Jul 18 22:58:50 2015 +0200
@@ -6,7 +6,7 @@
 Definition of bounded natural functors.
 *)
 
-section {* Definition of Bounded Natural Functors *}
+section \<open>Definition of Bounded Natural Functors\<close>
 
 theory BNF_Def
 imports BNF_Cardinal_Arithmetic Fun_Def_Base