diff --git a/thys/Birkhoff_Finite_Distributive_Lattices/ROOT b/thys/Birkhoff_Finite_Distributive_Lattices/ROOT
--- a/thys/Birkhoff_Finite_Distributive_Lattices/ROOT
+++ b/thys/Birkhoff_Finite_Distributive_Lattices/ROOT
@@ -1,12 +1,11 @@
 chapter AFP
 
 session Birkhoff_Finite_Distributive_Lattices (AFP) = "HOL" +
-  (* options [document = pdf, document_output = "output"] *)
   options [timeout = 300]
   sessions
     "HOL-Library"
   theories
     Birkhoff_Finite_Distributive_Lattices
   document_files
     "root.tex"
     "root.bib"
diff --git a/thys/MDP-Algorithms/ROOT b/thys/MDP-Algorithms/ROOT
--- a/thys/MDP-Algorithms/ROOT
+++ b/thys/MDP-Algorithms/ROOT
@@ -1,23 +1,22 @@
 chapter AFP
 session "MDP-Algorithms" (AFP) = "MDP-Rewards" +
-  options [document = pdf, document_output = "output", timeout = 600]
+  options [timeout = 600]
   sessions
     Gauss_Jordan Jordan_Normal_Form Perron_Frobenius "HOL-Data_Structures"
   directories
     code
     "code/lib"
   theories
     VI_Code_Export_Float
     VI_Code_Export_Rat
     GS_Code_Export_Float
     GS_Code_Export_Rat
     MPI_Code_Export_Float
     MPI_Code_Export_Rat
     PI_Code_Export_Float
     PI_Code_Export_Rat
     Fin_Code_Export_Float
     Fin_Code_Export_Rat
-
   document_files
     "root.bib"
     "root.tex"
diff --git a/thys/MDP-Rewards/ROOT b/thys/MDP-Rewards/ROOT
--- a/thys/MDP-Rewards/ROOT
+++ b/thys/MDP-Rewards/ROOT
@@ -1,8 +1,8 @@
 chapter AFP
 session "MDP-Rewards" (AFP) = "HOL-Probability" +
-  options [document = pdf, document_output = "output", timeout = 600]
+  options [timeout = 600]
   theories
     MDP_reward
   document_files
     "root.bib"
     "root.tex"
diff --git a/thys/Universal_Turing_Machine/ROOT b/thys/Universal_Turing_Machine/ROOT
--- a/thys/Universal_Turing_Machine/ROOT
+++ b/thys/Universal_Turing_Machine/ROOT
@@ -1,72 +1,70 @@
 chapter AFP
 
 session Universal_Turing_Machine (AFP) = HOL +
   options [timeout = 1200]
-
   sessions
     "HOL-Library"
   theories [document = false]
      "HOL-Library.Code_Target_Int"
      "HOL-Library.Code_Abstract_Nat"
      "HOL-Library.Code_Binary_Nat"
      "HOL-Library.Code_Target_Nat"
      "HOL-Library.Code_Target_Numeral"
 
-  theories [document = pdf]
+  theories
     "Turing"
     "Turing_aux"
     "BlanksDoNotMatter"
     "ComposableTMs"
     "ComposedTMs"
 
     "Numerals"
     "Numerals_Ex"
 
     "Turing_Hoare"
     "SemiIdTM"
     "Turing_HaltingConditions"
 
     "OneStrokeTM"
     "WeakCopyTM"
     "StrongCopyTM"
     "TuringDecidable"
     "TuringReducible"
     "SimpleGoedelEncoding"
     "HaltingProblems_K_H"
     "HaltingProblems_K_aux"
     "TuringComputable"
 
     (* ------------------- *)
 
     "DitherTM"
     "CopyTM"
     "TuringUnComputable_H2"
     "TuringUnComputable_H2_original"
 
     (* ------------------- *)
 
     "Abacus_Mopup"
     "Abacus"
     "Abacus_alt_Compile"
     "Abacus_Hoare"
 
     "Rec_Def"
     "Rec_Ex"
     "Recursive"
 
     "Recs_alt_Def"
     "Recs_alt_Ex"
 
     "UF"
     "UTM"
 
     (* ------------------- *)
 
     "GeneratedCode"
 
     (* ------------------- *)
 
-document_files
+  document_files
     "root.bib"
     "root.tex"
-