src/HOL/Library/Efficient_Nat.thy

--- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 10 19:09:21 2008 +0100
@@ -183,7 +183,9 @@
 val term_of_nat = HOLogic.mk_number HOLogic.natT;
 *}
 attach (test) {*
-fun gen_nat i = random_range 0 i;
+fun gen_nat i =
+  let val n = random_range 0 i
+  in (n, fn () => term_of_nat n) end;
 *}
 
 consts_code