diff -r 8c240fdeffcb -r 5840724b1d71 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Mon Sep 24 14:30:09 2018 +0200
@@ -279,7 +279,7 @@
 lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="(+)"]
   and simple_function_diff[intro, simp] = simple_function_compose2[where h="(-)"]
   and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
-  and simple_function_mult[intro, simp] = simple_function_compose2[where h="( * )"]
+  and simple_function_mult[intro, simp] = simple_function_compose2[where h="(*)"]
   and simple_function_div[intro, simp] = simple_function_compose2[where h="(/)"]
   and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
   and simple_function_max[intro, simp] = simple_function_compose2[where h=max]
@@ -760,7 +760,7 @@
     using assms by (intro simple_function_partition) auto
   also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ennreal))`space M.
     if snd y = 1 then fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A) else 0)"
-    by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="( * )"] arg_cong2[where f=emeasure] sum.cong)
+    by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="(*)"] arg_cong2[where f=emeasure] sum.cong)
   also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, 1::ennreal))`A. fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A))"
     using assms by (subst sum.If_cases) (auto intro!: simple_functionD(1) simp: eq)
   also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ennreal))`A. y * emeasure M (f -` {y} \<inter> space M \<inter> A))"