src/HOL/Analysis/Bochner_Integration.thy

   then have s'_eq_s: "\<And>i x. x \<in> space M \<Longrightarrow> s' i x = s i x"
     by simp
 
   have sf[measurable]: "\<And>i. simple_function M (s' i)"
     unfolding s'_def using s(1)
-    by (intro simple_function_compose2[where h="( *\<^sub>R)"] simple_function_indicator) auto
+    by (intro simple_function_compose2[where h="(*\<^sub>R)"] simple_function_indicator) auto
 
   { fix i
     have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
         (if z \<in> space M \<and> s' i z \<noteq> 0 then {s' i z} else {})"
       by (auto simp add: s'_def split: split_indicator)