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