--- 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)