all theories must be related to Reconstruction

--- a/src/HOL/Main.thy	Tue Dec 07 16:15:44 2004 +0100
+++ b/src/HOL/Main.thy	Tue Dec 07 16:16:10 2004 +0100
@@ -6,7 +6,7 @@
 header {* Main HOL *}
 
 theory Main
-    imports Map Infinite_Set Extraction Refute Reconstruction
+    imports Extraction Refute Reconstruction
 
 begin
 

--- a/src/HOL/Reconstruction.thy	Tue Dec 07 16:15:44 2004 +0100
+++ b/src/HOL/Reconstruction.thy	Tue Dec 07 16:16:10 2004 +0100
@@ -7,7 +7,7 @@
 header{*Attributes for Reconstructing External Resolution Proofs*}
 
 theory Reconstruction
-    imports Hilbert_Choice
+    imports Hilbert_Choice Map Infinite_Set
     files "Tools/res_lib.ML"
 	  "Tools/res_clause.ML"
 	  "Tools/res_skolem_function.ML"
@@ -18,6 +18,8 @@
 
 begin
 
+text{*Every theory of HOL must be a descendant or ancestor of this one!*}
+
 setup Reconstruction.setup
 
 end
\ No newline at end of file