--- a/src/HOL/Probability/Borel_Space.thy Mon Mar 09 11:32:32 2015 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Mon Mar 09 16:28:19 2015 +0000
@@ -1089,10 +1089,10 @@
lemma borel_measurable_of_real [measurable]: "(of_real :: _ \<Rightarrow> (_::real_normed_algebra)) \<in> borel_measurable borel"
by (intro borel_measurable_continuous_on1 continuous_intros)
-lemma borel_measurable_sin [measurable]: "sin \<in> borel_measurable borel"
+lemma borel_measurable_sin [measurable]: "(sin :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel"
by (intro borel_measurable_continuous_on1 continuous_intros)
-lemma borel_measurable_cos [measurable]: "cos \<in> borel_measurable borel"
+lemma borel_measurable_cos [measurable]: "(cos :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel"
by (intro borel_measurable_continuous_on1 continuous_intros)
lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"