src/HOL/NumberTheory/Quadratic_Reciprocity.thy

     by (auto simp add: zpower_zadd_distrib)
   also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
       nat(setsum (%x. ((x * q) div p)) P_set) =
         nat((setsum (%x. ((x * p) div q)) Q_set) +
           (setsum (%x. ((x * q) div p)) P_set))"
-    apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in
+    apply (rule_tac z = "setsum (%x. ((x * p) div q)) Q_set" in
       nat_add_distrib [symmetric])
     apply (auto simp add: S1_carda [symmetric] S2_carda [symmetric])
     done
   also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))"
     by (auto simp add: pq_sum_prop)