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