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