diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -8,6 +8,17 @@
 
 end; (*struct Nat*)
 
+structure Integer = 
+struct
+
+fun nat_aux n i =
+  (if IntInf.<= (i, (0 : IntInf.int)) then n
+    else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int))));
+
+fun nat i = nat_aux Nat.Zero_nat i;
+
+end; (*struct Integer*)
+
 structure Codegen = 
 struct
 
@@ -15,7 +26,7 @@
 
 val foobar_set : Nat.nat list =
   Nat.Zero_nat ::
-    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
+    (Nat.Suc Nat.Zero_nat :: (Integer.nat (2 : IntInf.int) :: []));
 
 end; (*struct Codegen*)