diff -r e54cf66928e6 -r 5e0455e29339 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Aug 23 12:44:52 2012 +0200
+++ b/src/HOL/ROOT	Thu Aug 23 12:55:23 2012 +0200
@@ -2,7 +2,11 @@
   description {* Classical Higher-order Logic *}
   options [document_graph]
   theories Complex_Main
-  files "document/root.bib" "document/root.tex"
+  files
+    "Tools/Quickcheck/Narrowing_Engine.hs"
+    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
+    "document/root.bib"
+    "document/root.tex"
 
 session "HOL-Base" = Pure +
   description {* Raw HOL base, with minimal tools *}
@@ -18,11 +22,17 @@
   description {* HOL side-entry for Main only, without Complex_Main *}
   options [document = false]
   theories Main
+  files
+    "Tools/Quickcheck/Narrowing_Engine.hs"
+    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 
 session "HOL-Proofs" = Pure +
   description {* HOL-Main with explicit proof terms *}
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Main
+  files
+    "Tools/Quickcheck/Narrowing_Engine.hs"
+    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 
 session "HOL-Library" in Library = HOL +
   description {* Classical Higher-order Logic -- batteries included *}