diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Wed Nov 08 13:48:29 2006 +0100
@@ -7,7 +7,7 @@
 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
 
 theory Hilbert_Choice
-imports NatArith
+imports Nat
 uses ("Tools/meson.ML") ("Tools/specification_package.ML")
 begin