--- a/src/HOL/Equiv_Relations.thy Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Equiv_Relations.thy Mon Feb 21 15:04:10 2005 +0100
@@ -327,7 +327,7 @@
apply assumption
apply simp
apply(fastsimp simp add:inj_on_def)
-apply (simp add:setsum_constant_nat)
+apply (simp add:setsum_constant)
done
ML