diff --git a/thys/FSM_Tests/ROOT b/thys/FSM_Tests/ROOT
--- a/thys/FSM_Tests/ROOT
+++ b/thys/FSM_Tests/ROOT
@@ -1,65 +1,65 @@
 chapter AFP
 
 session FSM_Tests (AFP) = "HOL-Library" + 
-  options [timeout = 600, document = pdf]
+  options [timeout = 600]
   sessions
     "Datatype_Order_Generator"
     "Containers"
     "Native_Word"
   directories
     "AdaptiveStateCounting"
     "EquivalenceTesting"
   theories
     "Util"
     "Util_Refined"
     "FSM_Impl"
     "FSM"
     "Product_FSM"
     "Distinguishability"
     "IO_Sequence_Set"
     "Minimisation"
     "Observability"
     "Prefix_Tree"
     "Prefix_Tree_Refined"
     "Prime_Transformation"
     "State_Cover"
     "OFSM_Tables_Refined"
     
     "EquivalenceTesting/Convergence"
     "EquivalenceTesting/Convergence_Graph"
     "EquivalenceTesting/Empty_Convergence_Graph"
     "EquivalenceTesting/H_Framework"
     "EquivalenceTesting/H_Method_Implementations"    
     "EquivalenceTesting/HSI_Method_Implementations"
     "EquivalenceTesting/Intermediate_Frameworks"
     "EquivalenceTesting/Intermediate_Implementations"
     "EquivalenceTesting/Pair_Framework"
     "EquivalenceTesting/Partial_S_Method_Implementations"
     "EquivalenceTesting/Simple_Convergence_Graph"
     "EquivalenceTesting/SPY_Framework"
     "EquivalenceTesting/SPY_Method_Implementations"    
     "EquivalenceTesting/SPYH_Method_Implementations"
     "EquivalenceTesting/Test_Suite_Representations_Refined"
     "EquivalenceTesting/Test_Suite_Representations"
     "EquivalenceTesting/W_Method_Implementations"
     "EquivalenceTesting/Wp_Method_Implementations"
     
     "AdaptiveStateCounting/Adaptive_Test_Case"
     "AdaptiveStateCounting/Backwards_Reachability_Analysis"
     "AdaptiveStateCounting/Helper_Algorithms"
     "AdaptiveStateCounting/Maximal_Path_Trie"
     "AdaptiveStateCounting/R_Distinguishability"    
     "AdaptiveStateCounting/State_Preamble"
     "AdaptiveStateCounting/State_Separator"
     "AdaptiveStateCounting/Test_Suite_Calculation"
     "AdaptiveStateCounting/Test_Suite_Calculation_Refined"
     "AdaptiveStateCounting/Test_Suite_IO"
     "AdaptiveStateCounting/Test_Suite"
     "AdaptiveStateCounting/Traversal_Set"
 
     "FSM_Code_Datatype"
     "Test_Suite_Generator_Code_Export"
   document_files
     "root.tex"
     "root.bib"
   export_files (in "code_export") [2] "FSM_Tests.Test_Suite_Generator_Code_Export:code**"
\ No newline at end of file