--- 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*)