prefer file dependencies wrt. specific theories;

--- a/src/HOL/Quickcheck_Narrowing.thy	Mon Oct 02 19:28:18 2017 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Oct 02 19:38:39 2017 +0200
@@ -192,6 +192,8 @@
 
 subsubsection \<open>Setting up the counterexample generator\<close>
 
+external_file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
+external_file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 ML_file "Tools/Quickcheck/narrowing_generators.ML"
 
 definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"

--- a/src/HOL/ROOT	Mon Oct 02 19:28:18 2017 +0200
+++ b/src/HOL/ROOT	Mon Oct 02 19:38:39 2017 +0200
@@ -7,9 +7,6 @@
   theories
     Main (global)
     Complex_Main (global)
-  files
-    "Tools/Quickcheck/Narrowing_Engine.hs"
-    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
   document_files
     "root.bib"
     "root.tex"
@@ -24,9 +21,6 @@
     "HOL-Library"
   theories
     "HOL-Library.Old_Datatype"
-  files
-    "Tools/Quickcheck/Narrowing_Engine.hs"
-    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 
 session "HOL-Library" (main timing) in Library = HOL +
   description {*
@@ -848,12 +842,6 @@
     SMT_Examples
     SMT_Word_Examples
     SMT_Tests
-  files
-    "Boogie_Dijkstra.certs"
-    "Boogie_Max.certs"
-    "SMT_Examples.certs"
-    "SMT_Word_Examples.certs"
-    "VCC_Max.certs"
 
 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   options [document = false]

--- a/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:28:18 2017 +0200
+++ b/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:38:39 2017 +0200
@@ -55,17 +55,20 @@
 declare [[smt_read_only_certificates = true]]
 
 
+external_file "Boogie_Max.certs"
 declare [[smt_certificates = "Boogie_Max.certs"]]
 
 boogie_file Boogie_Max
 
 
+external_file "Boogie_Dijkstra.certs"
 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
 
 boogie_file Boogie_Dijkstra
 
 
 declare [[z3_extensions = true]]
+external_file "VCC_Max.certs"
 declare [[smt_certificates = "VCC_Max.certs"]]
 
 boogie_file VCC_Max

--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Oct 02 19:28:18 2017 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Oct 02 19:38:39 2017 +0200
@@ -8,6 +8,7 @@
 imports Complex_Main
 begin
 
+external_file "SMT_Examples.certs"
 declare [[smt_certificates = "SMT_Examples.certs"]]
 declare [[smt_read_only_certificates = true]]