diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -7,16 +7,18 @@
 datatype nat = Zero_nat | Suc of nat;
 
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
-  | plus_nat (Suc m) n = Suc (plus_nat m n);
+  | plus_nat Zero_nat y = y;
 
-fun times_nat (Suc m) n = plus_nat n (times_nat m n);
+fun times_nat (Suc m) n = plus_nat n (times_nat m n)
+  | times_nat Zero_nat n = Zero_nat;
 
 end; (*struct Nat*)
 
 structure Codegen = 
 struct
 
-fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
+fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
+  | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
 
 end; (*struct Codegen*)