diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -803,7 +803,7 @@
   "setsum f A == if finite A then fold (op +) f 0 A else 0"
 
 abbreviation
-  Setsum  ("\<Sum>_" [1000] 999)
+  Setsum  ("\<Sum>_" [1000] 999) where
   "\<Sum>A == setsum (%x. x) A"
 
 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
@@ -1275,7 +1275,7 @@
   "setprod f A == if finite A then fold (op *) f 1 A else 1"
 
 abbreviation
-  Setprod  ("\<Prod>_" [1000] 999)
+  Setprod  ("\<Prod>_" [1000] 999) where
   "\<Prod>A == setprod (%x. x) A"
 
 syntax