# HG changeset patch
# User nipkow
# Date 1322475756 -3600
# Node ID 4f7c05990420cb2c2d09f7e96f2bd4c78a8cc6e6
# Parent  862d68ee10f3be11d794291e37d141c3919e2f7e
Hide Product_Type.Times - too precious an identifier

diff -r 862d68ee10f3 -r 4f7c05990420 src/HOL/Product_Type.thy
--- 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