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]