Plain, Main form meeting points in import hierarchy

--- a/src/HOL/ATP_Linkup.thy	Wed Jan 28 11:02:12 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy	Wed Jan 28 11:03:16 2009 +0100
@@ -7,7 +7,7 @@
 header {* The Isabelle-ATP Linkup *}
 
 theory ATP_Linkup
-imports Divides Record Hilbert_Choice
+imports Divides Record Hilbert_Choice Plain
 uses
   "Tools/polyhash.ML"
   "Tools/res_clause.ML"

--- a/src/HOL/Lubs.thy	Wed Jan 28 11:02:12 2009 +0100
+++ b/src/HOL/Lubs.thy	Wed Jan 28 11:03:16 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title       : Lubs.thy
-    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
 *)
@@ -7,7 +6,7 @@
 header{*Definitions of Upper Bounds and Least Upper Bounds*}
 
 theory Lubs
-imports Plain
+imports Plain Main
 begin
 
 text{*Thanks to suggestions by James Margetson*}

--- a/src/HOL/Parity.thy	Wed Jan 28 11:02:12 2009 +0100
+++ b/src/HOL/Parity.thy	Wed Jan 28 11:03:16 2009 +0100
@@ -5,7 +5,7 @@
 header {* Even and Odd for int and nat *}
 
 theory Parity
-imports Plain Presburger
+imports Plain Presburger Main
 begin
 
 class even_odd = 

--- a/src/HOL/Polynomial.thy	Wed Jan 28 11:02:12 2009 +0100
+++ b/src/HOL/Polynomial.thy	Wed Jan 28 11:03:16 2009 +0100
@@ -6,7 +6,7 @@
 header {* Univariate Polynomials *}
 
 theory Polynomial
-imports Plain SetInterval
+imports Plain SetInterval Main
 begin
 
 subsection {* Definition of type @{text poly} *}

--- a/src/HOL/Recdef.thy	Wed Jan 28 11:02:12 2009 +0100
+++ b/src/HOL/Recdef.thy	Wed Jan 28 11:03:16 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Recdef.thy
-    ID:         $Id$
     Author:     Konrad Slind and Markus Wenzel, TU Muenchen
 *)
 
 header {* TFL: recursive function definitions *}
 
 theory Recdef
-imports FunDef
+imports FunDef Plain
 uses
   ("Tools/TFL/casesplit.ML")
   ("Tools/TFL/utils.ML")

--- a/src/HOL/Relation_Power.thy	Wed Jan 28 11:02:12 2009 +0100
+++ b/src/HOL/Relation_Power.thy	Wed Jan 28 11:03:16 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Relation_Power.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1996  TU Muenchen
 *)
@@ -7,7 +6,7 @@
 header{*Powers of Relations and Functions*}
 
 theory Relation_Power
-imports Power Transitive_Closure
+imports Power Transitive_Closure Plain
 begin
 
 instance