diff --git a/thys/Adaptive_State_Counting/ROOT b/thys/Adaptive_State_Counting/ROOT
--- a/thys/Adaptive_State_Counting/ROOT
+++ b/thys/Adaptive_State_Counting/ROOT
@@ -1,18 +1,22 @@
 chapter AFP
 
 session Adaptive_State_Counting (AFP) = "Transition_Systems_and_Automata" +
   options [timeout = 1200]
   sessions
     "HOL-Hoare"
+  directories
+    "FSM"
+    "ATC"
+    "ASC"
   theories
-    "FSM/FSM"
-    "FSM/FSM_Product"
-    "ATC/ATC"
-    "ASC/ASC_LB"
-    "ASC/ASC_Suite"
-    "ASC/ASC_Sufficiency"
-    "ASC/ASC_Hoare"
-    "ASC/ASC_Example"
+    "FSM"
+    "FSM_Product"
+    "ATC"
+    "ASC_LB"
+    "ASC_Suite"
+    "ASC_Sufficiency"
+    "ASC_Hoare"
+    "ASC_Example"
   document_files
     "root.bib"
     "root.tex"
diff --git a/thys/Hybrid_Systems_VCs/ROOT b/thys/Hybrid_Systems_VCs/ROOT
--- a/thys/Hybrid_Systems_VCs/ROOT
+++ b/thys/Hybrid_Systems_VCs/ROOT
@@ -1,16 +1,19 @@
 chapter AFP
 
 session "Hybrid_Systems_VCs" (AFP) = "HOL-Analysis" +
   options [timeout = 1800]
   sessions
     Ordinary_Differential_Equations
     Transformer_Semantics
     KAD
+  directories
+    "PredicateTransformers"
+    "ModalKleeneAlgebra"
   theories
     "HS_VC_Examples"
-    "PredicateTransformers/HS_VC_PT_Examples"
-    "ModalKleeneAlgebra/HS_VC_MKA_Examples_rel"
-    "ModalKleeneAlgebra/HS_VC_MKA_Examples_ndfun"
+    "HS_VC_PT_Examples"
+    "HS_VC_MKA_Examples_rel"
+    "HS_VC_MKA_Examples_ndfun"
   document_files
     "root.bib"
     "root.tex"