--- a/src/HOL/Analysis/Finite_Product_Measure.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Sat Jan 05 17:24:33 2019 +0100
@@ -15,7 +15,7 @@
lemma%unimportant case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
by auto
-subsubsection%unimportant \<open>More about Function restricted by @{const extensional}\<close>
+subsubsection%unimportant \<open>More about Function restricted by \<^const>\<open>extensional\<close>\<close>
definition
"merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"