# HG changeset patch
# User paulson
# Date 997275130 -7200
# Node ID f4d10044a2cdc513c3a79b0d74a7b72b18c00a2c
# Parent  ec2c382ff4f0b5bcc1983d6b910529c6228b2ef2
Hilbert_Choice is needed only in Main itself

diff -r ec2c382ff4f0 -r f4d10044a2cd src/HOL/Datatype_Universe.thy
--- 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
diff -r ec2c382ff4f0 -r f4d10044a2cd src/HOL/Main.thy
--- 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]