diff -r 8007f10195af -r 6108dddad9f0 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Jan 16 21:53:44 2017 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Tue Jan 17 11:26:21 2017 +0100
@@ -17,7 +17,7 @@
 to each factor is continuous.
 
 To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
-'a. The product is then @{term "PiE I X"}, the set of elements from 'i to 'a such that the $i$-th
+'a. The product is then @{term "Pi\<^sub>E I X"}, the set of elements from 'i to 'a such that the $i$-th
 coordinate belongs to $X\;i$ for all $i \in I$.
 
 Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
@@ -696,7 +696,7 @@
 lemma product_topology_countable_basis:
   shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
           topological_basis K \<and> countable K \<and>
-          (\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
+          (\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
 proof -
   obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
     using ex_countable_basis by auto
@@ -708,7 +708,7 @@
     using that unfolding B2_def using B topological_basis_open by auto
 
   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
-  have i: "\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+  have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
     unfolding K_def using `\<And>U. U \<in> B2 \<Longrightarrow> open U` by auto
 
   have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
@@ -1335,11 +1335,11 @@
   "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
 proof
   obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
-            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
     using product_topology_countable_basis by fast
   have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
   proof -
-    obtain X where H: "k = PiE UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
+    obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
       using K(3)[OF `k \<in> K`] by blast
     show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
   qed