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" ("(_ \/ _)" [21, 20] 20) -syntax (HTML output) - "*" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) +type_notation (xsymbols) + "*" ("(_ \/ _)" [21, 20] 20) +type_notation (HTML output) + "*" ("(_ \/ _)" [21, 20] 20) consts Pair :: "'a \ 'b \ 'a \ 'b"