diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -809,12 +809,11 @@
 text \<open>
   A note on code generation: When defining some function containing a
   subterm @{term "fold_mset F"}, code generation is not automatic. When
-  interpreting locale @{text left_commutative} with @{text F}, the
+  interpreting locale \<open>left_commutative\<close> with \<open>F\<close>, the
   would be code thms for @{const fold_mset} become thms like
-  @{term "fold_mset F z {#} = z"} where @{text F} is not a pattern but
+  @{term "fold_mset F z {#} = z"} where \<open>F\<close> is not a pattern but
   contains defined symbols, i.e.\ is not a code thm. Hence a separate
-  constant with its own code thms needs to be introduced for @{text
-  F}. See the image operator below.
+  constant with its own code thms needs to be introduced for \<open>F\<close>. See the image operator below.
 \<close>
 
 
@@ -1083,7 +1082,7 @@
   qed
   then show "PROP ?P" "PROP ?Q" "PROP ?R"
   by (auto elim!: Set.set_insert)
-qed -- \<open>TODO: maybe define @{const mset_set} also in terms of @{const Abs_multiset}\<close>
+qed \<comment> \<open>TODO: maybe define @{const mset_set} also in terms of @{const Abs_multiset}\<close>
 
 lemma elem_mset_set[simp, intro]: "finite A \<Longrightarrow> x \<in># mset_set A \<longleftrightarrow> x \<in> A"
   by (induct A rule: finite_induct) simp_all
@@ -1349,7 +1348,7 @@
 
 text \<open>
   This lemma shows which properties suffice to show that a function
-  @{text "f"} with @{text "f xs = ys"} behaves like sort.
+  \<open>f\<close> with \<open>f xs = ys\<close> behaves like sort.
 \<close>
 
 lemma properties_for_sort_key:
@@ -2106,7 +2105,7 @@
 
 declare sorted_list_of_multiset_mset [code]
 
-lemma [code]: -- \<open>not very efficient, but representation-ignorant!\<close>
+lemma [code]: \<comment> \<open>not very efficient, but representation-ignorant!\<close>
   "mset_set A = mset (sorted_list_of_set A)"
   apply (cases "finite A")
   apply simp_all