src/HOL/Equiv_Relations.thy
changeset 35216 7641e8d831d2
parent 30198 922f944f03b2
child 35725 4d7e3cc9c52c
--- a/src/HOL/Equiv_Relations.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Equiv_Relations.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -328,7 +328,7 @@
    apply assumption
   apply simp
  apply(fastsimp simp add:inj_on_def)
-apply (simp add:setsum_constant)
+apply simp
 done
 
 end