# HG changeset patch
# User nipkow
# Date 1322500087 -3600
# Node ID d32ec2234efc66da7aec1a58b623a11eab61c36c
# Parent  ec6ba4b1f6d58175c6ade8d8b15a693e40ceeca4# Parent  4f7c05990420cb2c2d09f7e96f2bd4c78a8cc6e6
merged

diff -r ec6ba4b1f6d5 -r d32ec2234efc src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Nov 28 17:06:29 2011 +0100
+++ b/src/HOL/Product_Type.thy	Mon Nov 28 18:08:07 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