src/HOL/Library/Permutations.thy

--- a/src/HOL/Library/Permutations.thy	Tue Dec 20 14:43:41 2011 +0100
+++ b/src/HOL/Library/Permutations.thy	Tue Dec 20 14:43:42 2011 +0100
@@ -742,7 +742,6 @@
 apply metis
 done
 
-term setsum
 lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
 proof-
   let ?S = "{p . p permutes S}"