diff -r 5ddea758679b -r 69eb69659bf3 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Nov 19 17:04:29 2008 +0100
+++ b/src/HOL/SetInterval.thy	Wed Nov 19 17:54:55 2008 +0100
@@ -724,10 +724,10 @@
  ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
 
 translations
-  "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
-  "\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}"
-  "\<Sum>i\<le>n. t" == "setsum (\<lambda>i. t) {..n}"
-  "\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}"
+  "\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}"
+  "\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}"
+  "\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}"
+  "\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}"
 
 text{* The above introduces some pretty alternative syntaxes for
 summation over intervals: