--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Mon Feb 21 15:57:45 2005 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Mon Feb 21 18:04:28 2005 +0100
@@ -272,7 +272,7 @@
lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
- apply (auto simp add: S_def zmult_int setsum_constant_nat)
+ apply (auto simp add: S_def zmult_int setsum_constant)
done
lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}"