src/HOL/NumberTheory/IntFact.thy

--- a/src/HOL/NumberTheory/IntFact.thy	Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/NumberTheory/IntFact.thy	Wed Dec 03 10:49:34 2003 +0100
@@ -39,7 +39,7 @@
 
 lemma setprod_insert [simp]:
     "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
-  by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro])
+  by (simp add: setprod_def mult_left_commute LC.fold_insert [OF LC.intro])
 
 text {*
   \medskip @{term d22set} --- recursively defined set including all