diff -r 4f19b92ab6d7 -r 8e9100dcde52 src/HOL/Algebra/Algebra.thy
--- a/src/HOL/Algebra/Algebra.thy	Fri Apr 12 12:29:20 2019 +0100
+++ b/src/HOL/Algebra/Algebra.thy	Sat Apr 13 19:23:47 2019 +0100
@@ -2,6 +2,6 @@
 
 theory Algebra
   imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
-     Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
+     Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure
 begin
 end