src/HOL/Big_Operators.thy

 let
   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
         if x <> y then raise Match
         else
           let
-            val x' = Syntax_Trans.mark_bound x;
+            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 "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
+          in
+            Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
+          end
     | setsum_tr' _ = raise Match;
 in [(@{const_syntax setsum}, setsum_tr')] end
 *}
 
 lemma setsum_empty: