diff -r 1d43f86f48be -r e96292f32c3c src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Product_Type.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -226,11 +226,11 @@
 
 definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}"
 
-typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
+typedef ('a, 'b) prod ("(_ \<times>/ _)" [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
   unfolding prod_def by auto
 
-type_notation (xsymbols)
-  "prod"  ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (ASCII)
+  prod  (infixr "*" 20)
 
 definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
   "Pair a b = Abs_prod (Pair_Rep a b)"