src/HOL/NumberTheory/IntFact.thy

--- a/src/HOL/NumberTheory/IntFact.thy	Wed Jan 09 17:56:46 2002 +0100
+++ b/src/HOL/NumberTheory/IntFact.thy	Thu Jan 10 01:10:58 2002 +0100
@@ -40,7 +40,7 @@
 lemma setprod_insert [simp]:
     "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
   apply (unfold setprod_def)
-  apply (simp add: zmult_left_commute fold_insert [standard])
+  apply (simp add: zmult_left_commute LC.fold_insert)
   done