src/HOL/Hilbert_Choice.thy

--- a/src/HOL/Hilbert_Choice.thy	Fri Feb 15 16:09:10 2008 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Fri Feb 15 16:09:12 2008 +0100
@@ -7,7 +7,7 @@
 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
 
 theory Hilbert_Choice
-imports Nat
+imports Nat Wellfounded_Recursion
 uses ("Tools/meson.ML") ("Tools/specification_package.ML")
 begin