eliminated old-style no-document imports;

--- a/src/Doc/ROOT	Mon Oct 02 15:51:52 2017 +0200
+++ b/src/Doc/ROOT	Mon Oct 02 16:08:43 2017 +0200
@@ -48,7 +48,6 @@
   options [document_variants = "corec"]
   sessions
     Datatypes
-  theories [document = false] Datatypes.Setup
   theories Corec
   document_files (in "..")
     "prepare_document"
@@ -248,9 +247,6 @@
   options [document_variants = "sugar"]
   sessions
     "HOL-Library"
-  theories [document = false]
-    "HOL-Library.LaTeXsugar"
-    "HOL-Library.OptionalSugar"
   theories Sugar
   document_files (in "..")
     "prepare_document"

--- a/src/HOL/ROOT	Mon Oct 02 15:51:52 2017 +0200
+++ b/src/HOL/ROOT	Mon Oct 02 16:08:43 2017 +0200
@@ -121,8 +121,6 @@
     Exp demonstrates the use of iterated inductive definitions to reason about
     mutually recursive relations.
   *}
-  theories [document = false]
-    "HOL-Library.Old_Datatype"
   theories [quick_and_dirty]
     Common_Patterns
   theories
@@ -142,12 +140,6 @@
 
 session "HOL-IMP" (timing) in IMP = "HOL-Library" +
   options [document_variants = document]
-  theories [document = false]
-    "HOL-Library.While_Combinator"
-    "HOL-Library.Char_ord"
-    "HOL-Library.List_lexord"
-    "HOL-Library.Quotient_List"
-    "HOL-Library.Extended"
   theories
     BExp
     ASM
@@ -200,8 +192,6 @@
     "HOL-Number_Theory"
   theories [document = false]
     Less_False
-    "HOL-Library.Multiset"
-    "HOL-Number_Theory.Fib"
   theories
     Sorting
     Balance
@@ -227,11 +217,6 @@
   *}
   sessions
     "HOL-Algebra"
-  theories [document = false]
-    "HOL-Library.FuncSet"
-    "HOL-Library.Multiset"
-    "HOL-Algebra.Ring"
-    "HOL-Algebra.FiniteProduct"
   theories
     Number_Theory
   document_files
@@ -310,11 +295,6 @@
 
     The Isabelle Algebraic Library.
   *}
-  theories [document = false]
-    (* Preliminaries from set and number theory *)
-    "HOL-Library.FuncSet"
-    "HOL-Computational_Algebra.Primes"
-    "HOL-Library.Permutation"
   theories
     (* Orders and Lattices *)
     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
@@ -403,10 +383,6 @@
 
 session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" +
   options [print_mode = "iff,no_brackets"]
-  theories [document = false]
-    "HOL-Library.Countable"
-    "HOL-Library.Monad_Syntax"
-    "HOL-Library.LaTeXsugar"
   theories Imperative_HOL_ex
   document_files "root.bib" "root.tex"
 
@@ -435,11 +411,6 @@
   sessions
     "HOL-Library"
     "HOL-Computational_Algebra"
-  theories [document = false]
-    "HOL-Library.Code_Target_Numeral"
-    "HOL-Library.Monad_Syntax"
-    "HOL-Computational_Algebra.Primes"
-    "HOL-Library.Open_State_Syntax"
   theories
     Greatest_Common_Divisor
     Warshall
@@ -490,8 +461,6 @@
   *}
   sessions
     "HOL-Eisbach"
-  theories [document = false]
-    "HOL-Library.While_Combinator"
   theories
     MicroJava
   document_files
@@ -653,9 +622,6 @@
     Miscellaneous Isabelle/Isar examples.
   *}
   options [quick_and_dirty]
-  theories [document = false]
-    "HOL-Library.Lattice_Syntax"
-    "HOL-Computational_Algebra.Primes"
   theories
     Knaster_Tarski
     Peirce
@@ -694,8 +660,6 @@
   description {*
     Verification of the SET Protocol.
   *}
-  theories [document = false]
-    "HOL-Library.Nat_Bijection"
   theories
     SET_Protocol
   document_files "root.tex"
@@ -745,12 +709,6 @@
     ATP_Problem_Import
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
-  theories [document = false]
-    "HOL-Library.Countable"
-    "HOL-Library.Permutation"
-    "HOL-Library.Order_Continuity"
-    "HOL-Library.Diagonal_Subsequence"
-    "HOL-Library.Finite_Map"
   theories
     Probability (global)
   document_files "root.tex"
@@ -1073,9 +1031,6 @@
   *}
   sessions
     "HOL-Library"
-  theories [document = false]
-    "HOL-Library.Nat_Bijection"
-    "HOL-Library.Countable"
   theories
     HOLCF (global)
   document_files "root.tex"