diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/ROOT	Thu Jun 14 14:23:38 2018 +0100
@@ -294,22 +294,16 @@
   theories
     (* Orders and Lattices *)
     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
-
     (* Groups *)
     FiniteProduct        (* Product operator for commutative groups *)
     Sylow                (* Sylow's theorem *)
     Bij                  (* Automorphism Groups *)
-    More_Group
-    More_Finite_Product
     Multiplicative_Group
     Zassenhaus            (* The Zassenhaus lemma *)
-
-
     (* Rings *)
     Divisibility         (* Rings *)
     IntRing              (* Ideals and residue classes *)
     UnivPoly             (* Polynomials *)
-    More_Ring
   document_files "root.bib" "root.tex"
 
 session "HOL-Auth" (timing) in Auth = "HOL-Library" +