diff -r 7b4fb2a2c75e -r eea3c9048c7a doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -7,11 +7,11 @@
 datatype nat = Zero_nat | Succ_nat of nat;
 
 fun less_nat Zero_nat (Succ_nat n) = true
-  | less_nat na Zero_nat = false
-  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
+  | less_nat n Zero_nat = false
+  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
 
 fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
-  | minus_nat Zero_nat na = Zero_nat
+  | minus_nat Zero_nat n = Zero_nat
   | minus_nat y Zero_nat = y;
 
 end; (*struct IntDef*)
@@ -21,12 +21,11 @@
 
 fun pick ((k, v) :: xs) n =
   (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k))
-  | pick (x :: xsa) na =
+  | pick (x :: xs) n =
     let
       val (ka, va) = x;
     in
-      (if IntDef.less_nat na ka then va
-        else pick xsa (IntDef.minus_nat na ka))
+      (if IntDef.less_nat n ka then va else pick xs (IntDef.minus_nat n ka))
     end;
 
 end; (*struct Codegen*)