--- a/src/HOL/Big_Operators.thy Sat Sep 29 16:51:04 2012 +0200
+++ b/src/HOL/Big_Operators.thy Sat Sep 29 18:23:46 2012 +0200
@@ -201,10 +201,12 @@
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
*}