diff -r c38d8f139bbc -r 4257a7f2bf39 src/HOL/ex/Seq.thy
--- a/src/HOL/ex/Seq.thy	Tue Oct 07 21:01:31 2014 +0200
+++ b/src/HOL/ex/Seq.thy	Tue Oct 07 21:11:18 2014 +0200
@@ -2,7 +2,7 @@
     Author:     Makarius
 *)
 
-header {* Finite sequences *}
+header \<open>Finite sequences\<close>
 
 theory Seq
 imports Main