include imports that morally belong to Main and are used in HOL-Proofs applications;

--- a/src/HOL/ROOT	Fri Apr 21 11:21:59 2017 +0200
+++ b/src/HOL/ROOT	Fri Apr 21 11:38:45 2017 +0200
@@ -21,7 +21,10 @@
   options [document = false, theory_qualifier = "HOL",
     quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
   sessions "HOL-Library"
-  theories "HOL-Library.Old_Datatype"
+  theories
+    GCD
+    Binomial
+    "HOL-Library.Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"