more basic file dependencies -- no load command here;

--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Aug 23 12:44:52 2012 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Aug 23 12:55:23 2012 +0200
@@ -5,9 +5,6 @@
 theory Quickcheck_Narrowing
 imports Quickcheck_Exhaustive
 keywords "find_unused_assms" :: diag
-uses  (* FIXME session files *)
-  ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
-  ("Tools/Quickcheck/Narrowing_Engine.hs")
 begin
 
 subsection {* Counterexample generator *}

--- 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 *}

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Aug 23 12:44:52 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Aug 23 12:55:23 2012 +0200
@@ -202,12 +202,10 @@
 (** invocation of Haskell interpreter **)
 
 val narrowing_engine =
-  Context.>>> (Context.map_theory_result
-    (Thy_Load.use_file (Path.explode "Tools/Quickcheck/Narrowing_Engine.hs")))
+  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
 
 val pnf_narrowing_engine =
-  Context.>>> (Context.map_theory_result
-    (Thy_Load.use_file (Path.explode "Tools/Quickcheck/PNF_Narrowing_Engine.hs")))
+  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
 
 fun exec verbose code =
   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)