src/HOL/Big_Operators.thy

--- a/src/HOL/Big_Operators.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Big_Operators.thy	Sat May 25 15:37:53 2013 +0200
@@ -370,7 +370,7 @@
             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 *}