diff -r 010c26e24c72 -r aa58872267ee src/HOL/Library/Tree_Multiset.thy
--- a/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 17:33:22 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 17:54:09 2015 +0200
@@ -1,14 +1,14 @@
 (* Author: Tobias Nipkow *)
 
-section {* Multiset of Elements of Binary Tree *}
+section \<open>Multiset of Elements of Binary Tree\<close>
 
 theory Tree_Multiset
 imports Multiset Tree
 begin
 
-text{* Kept separate from theory @{theory Tree} to avoid importing all of
+text\<open>Kept separate from theory @{theory Tree} to avoid importing all of
 theory @{theory Multiset} into @{theory Tree}. Should be merged if
-@{theory Multiset} ever becomes part of @{theory Main}. *}
+@{theory Multiset} ever becomes part of @{theory Main}.\<close>
 
 fun mset_tree :: "'a tree \<Rightarrow> 'a multiset" where
 "mset_tree Leaf = {#}" |