diff -r e9ab4ad7bd15 -r 23307fd33906 src/HOL/Data_Structures/AVL_Map.thy
--- a/src/HOL/Data_Structures/AVL_Map.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/Data_Structures/AVL_Map.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -23,7 +23,7 @@
    GT \<Rightarrow> balL l (a,b) (delete x r))"
 
 
-subsection {* Functional Correctness Proofs *}
+subsection \<open>Functional Correctness Proofs\<close>
 
 theorem inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"