diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Tue Dec 29 23:50:44 2015 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Wed Dec 30 11:21:54 2015 +0100
@@ -187,7 +187,7 @@
   using open_restricted_space[of "\<lambda>x. \<not> P x"]
   unfolding closed_def by (rule back_subst) auto
 
-lemma tendsto_proj: "((\<lambda>x. x) ---> a) F \<Longrightarrow> ((\<lambda>x. (x)\<^sub>F i) ---> (a)\<^sub>F i) F"
+lemma tendsto_proj: "((\<lambda>x. x) \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. (x)\<^sub>F i) \<longlongrightarrow> (a)\<^sub>F i) F"
   unfolding tendsto_def
 proof safe
   fix S::"'b set"