diff -r 797ed46d724b -r 290bc97038c7 src/HOL/NumberTheory/Int2.thy
--- a/src/HOL/NumberTheory/Int2.thy	Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/NumberTheory/Int2.thy	Thu Dec 09 18:30:59 2004 +0100
@@ -178,7 +178,7 @@
 by (frule_tac m = m in zcong_not_zero, auto)
 
 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
-    ==> zgcd (gsetprod id A,y) = 1";
+    ==> zgcd (setprod id A,y) = 1";
   by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)
 
 (*****************************************************************)