adding Enum to HOL-Main image and removing it from HOL-Library

--- a/src/HOL/Enum.thy	Mon Nov 22 11:34:55 2010 +0100
+++ b/src/HOL/Enum.thy	Mon Nov 22 11:34:56 2010 +0100
@@ -3,7 +3,7 @@
 header {* Finite types as explicit enumerations *}
 
 theory Enum
-imports Map Main
+imports Map String
 begin
 
 subsection {* Class @{text enum} *}

--- a/src/HOL/IsaMakefile	Mon Nov 22 11:34:55 2010 +0100
+++ b/src/HOL/IsaMakefile	Mon Nov 22 11:34:56 2010 +0100
@@ -246,6 +246,7 @@
   Divides.thy \
   DSequence.thy \
   Equiv_Relations.thy \
+  Enum.thy \
   Groebner_Basis.thy \
   Hilbert_Choice.thy \
   Int.thy \
@@ -416,7 +417,7 @@
   Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
   Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
   Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
-  Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy	\
+  Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
   Library/Executable_Set.thy Library/Float.thy				\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
   Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy		\

--- a/src/HOL/Library/Library.thy	Mon Nov 22 11:34:55 2010 +0100
+++ b/src/HOL/Library/Library.thy	Mon Nov 22 11:34:56 2010 +0100
@@ -14,7 +14,6 @@
   Countable
   Diagonalize
   Dlist
-  Enum
   Eval_Witness
   Float
   Formal_Power_Series

--- a/src/HOL/Quickcheck.thy	Mon Nov 22 11:34:55 2010 +0100
+++ b/src/HOL/Quickcheck.thy	Mon Nov 22 11:34:56 2010 +0100
@@ -3,7 +3,7 @@
 header {* A simple counterexample generator *}
 
 theory Quickcheck
-imports Random Code_Evaluation
+imports Random Code_Evaluation Enum
 uses ("Tools/quickcheck_generators.ML")
 begin