# HG changeset patch
# User wenzelm
# Date 1727860667 -7200
# Node ID 9dde09c065e1aa74d1fbd41bfd160597602e0ae3
# Parent  21faacc45c0c98f0232911867cb7061270a8b4f5
tuned;

diff -r 21faacc45c0c -r 9dde09c065e1 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 02 11:08:45 2024 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 02 11:17:47 2024 +0200
@@ -999,10 +999,11 @@
 definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set"
   where "Sigma A B \<equiv> \<Union>x\<in>A. \<Union>y\<in>B x. {Pair x y}"
 
-abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr \<open>\<times>\<close> 80)
+context
+begin
+qualified abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr \<open>\<times>\<close> 80)
   where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)"
-
-hide_const (open) Times
+end
 
 bundle no_Set_Product_syntax begin
 no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)