--- a/src/HOL/Probability/Characteristic_Functions.thy Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy Wed Jul 17 14:02:42 2019 +0100
@@ -91,7 +91,7 @@
qed
lemma (in real_distribution) char_measurable [measurable]: "char M \<in> borel_measurable borel"
- by (auto intro!: borel_measurable_continuous_on1 continuous_at_imp_continuous_on isCont_char)
+ by (auto intro!: borel_measurable_continuous_onI continuous_at_imp_continuous_on isCont_char)
subsection \<open>Independence\<close>