--- 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)"