# HG changeset patch
# User wenzelm
# Date 1166108889 -3600
# Node ID c898fdd6ff2dfdea3e17d8ae77843a137af3c7d2
# Parent  da545169fe06e965a1bdb7cb6e4196a8931e929d
proper use of IntInf instead of InfInf;

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;