src/HOL/Big_Operators.thy

             val P' = subst_bound (x', P);
           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
+in [(@{const_syntax setsum}, K setsum_tr')] end
 *}
 
 text {* TODO These are candidates for generalization *}
 
 context comm_monoid_add