src/HOL/Groups_Big.thy

 syntax
   "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum> Collect\<close>\<close>\<Sum>_ | (_)./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_qsum" == sum
-
 translations
   "\<Sum>x|P. t" => "CONST sum (\<lambda>x. t) {x. P}"
-
 print_translation \<open>
-  let
-    fun sum_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>_qsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
-            end
-      | sum_tr' _ = raise Match;
-  in [(\<^const_syntax>\<open>sum\<close>, K sum_tr')] end
+  [(\<^const_syntax>\<open>sum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qsum\<close>))]
 \<close>
 
 
 subsubsection \<open>Properties in more restricted classes of structures\<close>
 

 syntax
   "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=2 notation=\<open>binder \<Prod> Collect\<close>\<close>\<Prod>_ | (_)./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_qprod" == prod
-
 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
+  [(\<^const_syntax>\<open>prod\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qprod\<close>))]
 \<close>
 
 context comm_monoid_mult
 begin