proper use of IntInf instead of InfInf;
authorwenzelm
Thu, 14 Dec 2006 16:08:09 +0100
changeset 21846 c898fdd6ff2d
parent 21845 da545169fe06
child 21847 59a68ed9f2f2
proper use of IntInf instead of InfInf;
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;