diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Big_Operators.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -86,10 +86,10 @@
         if x <> y then raise Match
         else
           let
-            val x' = Syntax.mark_bound x;
+            val x' = Syntax_Trans.mark_bound x;
             val t' = subst_bound (x', t);
             val P' = subst_bound (x', P);
-          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
+          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
     | setsum_tr' _ = raise Match;
 in [(@{const_syntax setsum}, setsum_tr')] end
 *}