diff -r 1c2b9df41e98 -r 84a21cf15923 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Wed Nov 22 10:20:16 2006 +0100
+++ b/src/HOL/PreList.thy	Wed Nov 22 10:20:17 2006 +0100
@@ -8,7 +8,7 @@
 
 theory PreList
 imports Wellfounded_Relations Presburger Relation_Power SAT
-  Hilbert_Choice FunDef Extraction
+  FunDef Extraction
 begin
 
 text {*