Hilbert_Choice is needed only in Main itself

--- a/src/HOL/Datatype_Universe.thy	Wed Aug 08 14:51:30 2001 +0200
+++ b/src/HOL/Datatype_Universe.thy	Wed Aug 08 14:52:10 2001 +0200
@@ -9,13 +9,13 @@
 Could <*> be generalized to a general summation (Sigma)?
 *)
 
-Datatype_Universe = NatArith + Sum_Type + Hilbert_Choice +
+Datatype_Universe = NatArith + Sum_Type + 
 
 
 (** lists, trees will be sets of nodes **)
 
 typedef (Node)
-  ('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
+  ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
 
 types
   'a item = ('a, unit) node set

--- a/src/HOL/Main.thy	Wed Aug 08 14:51:30 2001 +0200
+++ b/src/HOL/Main.thy	Wed Aug 08 14:52:10 2001 +0200
@@ -7,7 +7,7 @@
 Note that theory PreList already includes most HOL theories.
 *)
 
-theory Main = Map + String:
+theory Main = Map + String + Hilbert_Choice:
 
 (*belongs to theory List*)
 declare lists_mono [mono]