Hide Product_Type.Times - too precious an identifier

--- a/src/HOL/Product_Type.thy	Sun Nov 27 23:12:03 2011 +0100
+++ b/src/HOL/Product_Type.thy	Mon Nov 28 11:22:36 2011 +0100
@@ -897,6 +897,8 @@
 notation (HTML output)
   Times  (infixr "\<times>" 80)
 
+hide_const (open) Times
+
 syntax
   "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
 translations