src/HOL/Algebra/Algebra.thy

--- a/src/HOL/Algebra/Algebra.thy	Thu Apr 04 16:38:45 2019 +0100
+++ b/src/HOL/Algebra/Algebra.thy	Fri Apr 05 11:21:53 2019 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Algebra/Algebra.thy *)
 
 theory Algebra
-  imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Product_Groups
+  imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
 begin
 end