diff --git a/thys/Buchi_Complementation/ROOT b/thys/Buchi_Complementation/ROOT
--- a/thys/Buchi_Complementation/ROOT
+++ b/thys/Buchi_Complementation/ROOT
@@ -1,15 +1,15 @@
 chapter AFP
 
 session Buchi_Complementation (AFP) = "Transition_Systems_and_Automata" +
   options [timeout = 1200]
   theories
     "Complementation"
     "Complementation_Implement"
     "Complementation_Final"
   theories [condition = ISABELLE_MLTON]
     "Complementation_Build"
   document_files
     "root.tex"
     "root.bib"
   export_files (in ".") [1]
-    "Buchi_Complementation.Complementation_Build:**"
+    "Buchi_Complementation.Complementation_Build:code/**"
diff --git a/thys/Diophantine_Eqns_Lin_Hom/ROOT b/thys/Diophantine_Eqns_Lin_Hom/ROOT
--- a/thys/Diophantine_Eqns_Lin_Hom/ROOT
+++ b/thys/Diophantine_Eqns_Lin_Hom/ROOT
@@ -1,17 +1,17 @@
 chapter AFP
 
 session Diophantine_Eqns_Lin_Hom (AFP) = HOL +
   options [timeout = 600]
   theories
     List_Vector
     Linear_Diophantine_Equations
     Sorted_Wrt
     Minimize_Wrt
     Algorithm
   theories [document = false, condition = ISABELLE_GHC]
     Solver_Code
   document_files
     "root.bib"
     "root.tex"
   export_files (in ".") [2]
-    "Diophantine_Eqns_Lin_Hom.Solver_Code:**"
+    "Diophantine_Eqns_Lin_Hom.Solver_Code:code/**"
diff --git a/thys/LTL/ROOT b/thys/LTL/ROOT
--- a/thys/LTL/ROOT
+++ b/thys/LTL/ROOT
@@ -1,20 +1,20 @@
 chapter AFP
 
 session LTL (AFP) = "HOL-Library" +
   options [timeout = 600]
   sessions
     Boolean_Expression_Checkers
   directories
     "example"
   theories
     LTL
     Rewriting
     Equivalence_Relations
     Disjunctive_Normal_Form
     Code_Equations
     "example/Example"
   document_files
     "root.tex"
     "root.bib"
   export_files (in "example") [2]
-    "LTL.Example:**"
+    "LTL.Example:code/**"
diff --git a/thys/LTL_Master_Theorem/ROOT b/thys/LTL_Master_Theorem/ROOT
--- a/thys/LTL_Master_Theorem/ROOT
+++ b/thys/LTL_Master_Theorem/ROOT
@@ -1,25 +1,25 @@
 chapter AFP
 
 session LTL_Master_Theorem (AFP) = "Transition_Systems_and_Automata" +
   options [timeout = 600]
   sessions
     LTL
     Deriving
   directories
     "Logical_Characterization"
     "LTL_to_DRA"
   theories
     "Logical_Characterization/Master_Theorem"
     "Logical_Characterization/Asymmetric_Master_Theorem"
     "Logical_Characterization/Restricted_Master_Theorem"
 
     "LTL_to_DRA/DRA_Construction"
     "LTL_to_DRA/DRA_Instantiation"
     "LTL_to_DRA/DRA_Implementation"
 
     Code_Export
   document_files
     "root.tex"
     "root.bib"
   export_files (in ".") [1]
-    "LTL_Master_Theorem.Code_Export:**"
+    "LTL_Master_Theorem.Code_Export:code/**"
diff --git a/thys/LTL_Normal_Form/ROOT b/thys/LTL_Normal_Form/ROOT
--- a/thys/LTL_Normal_Form/ROOT
+++ b/thys/LTL_Normal_Form/ROOT
@@ -1,15 +1,15 @@
 chapter AFP
 
 session LTL_Normal_Form (AFP) = "LTL" +
   options [timeout = 600]
   sessions
     LTL_Master_Theorem
   theories
     "Normal_Form"
     "Normal_Form_Complexity"
     "Normal_Form_Code_Export"
   document_files
     "root.tex"
     "root.bib"
   export_files (in ".") [1]
-    "LTL_Normal_Form.Normal_Form_Code_Export:**"
+    "LTL_Normal_Form.Normal_Form_Code_Export:code/**"
diff --git a/thys/PAC_Checker/ROOT b/thys/PAC_Checker/ROOT
--- a/thys/PAC_Checker/ROOT
+++ b/thys/PAC_Checker/ROOT
@@ -1,37 +1,37 @@
 chapter AFP
 
 session PAC_Checker (AFP) = "Sepref_IICF" +
   description \<open>PAC proof checker\<close>
   options
     [timeout = 2700]
   sessions
     "HOL-Library"
     "HOL-Algebra"
     "Polynomials"
     Nested_Multisets_Ordinals
   theories
     PAC_More_Poly
     Finite_Map_Multiset
     WB_Sort
     More_Loops
     PAC_Specification
     PAC_Map_Rel
     PAC_Checker_Specification
     PAC_Checker_Relation
     PAC_Polynomials
     PAC_Polynomials_Term
     PAC_Polynomials_Operations
     PAC_Assoc_Map_Rel
     PAC_Map_Rel
     PAC_Checker
     PAC_Checker_Init
     PAC_Version
     PAC_Checker_Synthesis
   theories [condition=ISABELLE_MLTON]
     PAC_Checker_MLton
   document_files
     "root.tex"
     "root.bib"
   export_files (in "code") [1]
-    "PAC_Checker.PAC_Checker_MLton:**"
+    "PAC_Checker.PAC_Checker_MLton:code/**"