--- a/src/HOL/NumberTheory/IntFact.thy Wed Jul 24 22:14:42 2002 +0200
+++ b/src/HOL/NumberTheory/IntFact.thy Wed Jul 24 22:15:55 2002 +0200
@@ -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, OF LC_axioms.intro])
+ by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro])
text {*
\medskip @{term d22set} --- recursively defined set including all