| changeset 17782 | b3846df9d643 |
| parent 17761 | 2c42d0a94f58 |
| child 18423 | d7859164447f |
--- a/src/HOL/Finite_Set.thy Fri Oct 07 22:59:18 2005 +0200 +++ b/src/HOL/Finite_Set.thy Fri Oct 07 22:59:19 2005 +0200 @@ -840,7 +840,7 @@ parse_translation {* let - fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A + fun Setsum_tr [A] = Syntax.const "setsum" $ Term.absdummy (dummyT, Bound 0) $ A in [("_Setsum", Setsum_tr)] end; *}