# HG changeset patch
# User wenzelm
# Date 1724593983 -7200
# Node ID 1d8ce19d7d71789a6c335e52fcc3fc6dd4edb3bb
# Parent  47c0aa388621d34f3599b3f07f70155c193080b2
proper translation for "_qprod", following "_qsum" (see also e14b89d6ef13 and fa7d27ef7e59);

diff -r 47c0aa388621 -r 1d8ce19d7d71 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Aug 25 15:40:07 2024 +0200
+++ b/src/HOL/Groups_Big.thy	Sun Aug 25 15:53:03 2024 +0200
@@ -1445,6 +1445,22 @@
 translations
   "\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}"
 
+print_translation \<open>
+  let
+    fun prod_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P)] =
+          if x <> y then raise Match
+          else
+            let
+              val x' = Syntax_Trans.mark_bound_body (x, Tx);
+              val t' = subst_bound (x', t);
+              val P' = subst_bound (x', P);
+            in
+              Syntax.const \<^syntax_const>\<open>_qprod\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
+            end
+      | prod_tr' _ = raise Match;
+  in [(\<^const_syntax>\<open>prod\<close>, K prod_tr')] end
+\<close>
+
 context comm_monoid_mult
 begin