src/HOL/Library/Tree.thy

--- a/src/HOL/Library/Tree.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Tree.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -146,7 +146,7 @@
   (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
 
 
-subsection "Function @{text mirror}"
+subsection "Function \<open>mirror\<close>"
 
 fun mirror :: "'a tree \<Rightarrow> 'a tree" where
 "mirror \<langle>\<rangle> = Leaf" |