src/HOL/Algebra/Divisibility.thy
changeset 28600 54352ed7114f
parent 28599 12d914277b8d
child 28823 dcbef866c9e2
--- a/src/HOL/Algebra/Divisibility.thy	Wed Oct 15 15:44:15 2008 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Oct 15 16:06:59 2008 +0200
@@ -1344,7 +1344,6 @@
 by (fast dest: e)
 
 lemma (in monoid) factorsI:
-  fixes G (structure)
   assumes "\<forall>f\<in>set fs. irreducible G f"
     and "foldr (op \<otimes>) fs \<one> = a"
   shows "factors G fs a"