# HG changeset patch
# User haftmann
# Date 1164187217 -3600
# Node ID 84a21cf15923dc2bdb40caecb0642cb3a229061f
# Parent  1c2b9df41e985645520f8ae3f1dcaee62ff9539a
does not import Hilber_Choice any longer

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 {*