src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy

--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Tue Nov 03 11:20:21 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Tue Nov 10 14:18:41 2015 +0000
@@ -274,7 +274,7 @@
 
 lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   using P_set_card Q_set_card P_set_finite Q_set_finite
-  by (auto simp add: S_def zmult_int)
+  by (simp add: S_def)
 
 lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
   by (auto simp add: S1_def S2_def)