diff -r da545169fe06 -r c898fdd6ff2d src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Thu Dec 14 15:31:22 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Thu Dec 14 16:08:09 2006 +0100
@@ -140,7 +140,7 @@
 types_code
   nat ("int")
 attach (term_of) {*
-val term_of_nat = HOLogic.mk_number HOLogic.natT o InfInf.fromInt;
+val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt;
 *}
 attach (test) {*
 fun gen_nat i = random_range 0 i;