diff -r 3f8d2834b2c4 -r 113c9516a2d7 src/HOL/NumberTheory/Gauss.thy
--- a/src/HOL/NumberTheory/Gauss.thy	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy	Mon Oct 09 02:19:51 2006 +0200
@@ -308,7 +308,7 @@
 lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   apply (auto simp add: C_def)
   apply (insert finite_B SR_B_inj)
-  apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id [symmetric], auto)
+  apply (frule_tac f = "StandardRes p" in setprod_reindex_id [symmetric], auto)
   apply (rule setprod_same_function_zcong)
   apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   done