src/HOL/Big_Operators.thy
changeset 42284 326f57825e1a
parent 41550 efa734d9b221
child 42871 1c0b99f950d9
     1.1 --- a/src/HOL/Big_Operators.thy	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/src/HOL/Big_Operators.thy	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -86,10 +86,10 @@
     1.4          if x <> y then raise Match
     1.5          else
     1.6            let
     1.7 -            val x' = Syntax.mark_bound x;
     1.8 +            val x' = Syntax_Trans.mark_bound x;
     1.9              val t' = subst_bound (x', t);
    1.10              val P' = subst_bound (x', P);
    1.11 -          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
    1.12 +          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
    1.13      | setsum_tr' _ = raise Match;
    1.14  in [(@{const_syntax setsum}, setsum_tr')] end
    1.15  *}