diff -r 1822da5446bc -r 72fcf0832cfe doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Tue Oct 23 14:00:06 2007 +0200
@@ -3,6 +3,8 @@
 
 datatype nat = Suc of nat | Zero_nat;
 
+val one_nat : nat = Suc Zero_nat;
+
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
   | plus_nat Zero_nat n = n;
 
@@ -15,6 +17,6 @@
 struct
 
 fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
-  | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
+  | fac Nat.Zero_nat = Nat.one_nat;
 
 end; (*struct Codegen*)