diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Merge_Poly.thy
--- a/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,13 +6,13 @@
 Tests polymorphic merges.
 *)
 
-section {* Tests Polymorphic Merges *}
+section \<open>Tests Polymorphic Merges\<close>
 
 theory Merge_Poly
 imports "~~/src/HOL/Library/BNF_Corec"
 begin
 
-subsection {* A Monomorphic Example *}
+subsection \<open>A Monomorphic Example\<close>
 
 codatatype r = R (rhd: nat) (rtl: r)
 
@@ -46,7 +46,7 @@
   "id_rx r = f1 (f2 (f3 (R (rhd r) (id_rx (rtl r)))))"
 
 
-subsection {* The Polymorphic Version *}
+subsection \<open>The Polymorphic Version\<close>
 
 codatatype 'a s = S (shd: 'a) (stl: "'a s")