diff -r c9b9d4fc270d -r ad039d29e01c src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOL/Product_Type.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -142,10 +142,10 @@
     by rule+
 qed
 
-syntax (xsymbols)
-  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
-syntax (HTML output)
-  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (xsymbols)
+  "*"  ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (HTML output)
+  "*"  ("(_ \<times>/ _)" [21, 20] 20)
 
 consts
   Pair     :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"