# HG changeset patch
# User ballarin
# Date 1224079619 -7200
# Node ID 54352ed7114fcb9cdfba9182c72cf4e9de589e81
# Parent  12d914277b8da44849fbd306b5388921ed11a2df
Removed 'includes' (fixed).

diff -r 12d914277b8d -r 54352ed7114f src/HOL/Algebra/Divisibility.thy
--- 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"