1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 15:29:44 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 17:11:09 2007 +0100
     1.3 @@ -6,13 +6,9 @@
     1.4  
     1.5  datatype nat = Zero_nat | Suc of nat;
     1.6  
     1.7 -fun less_nat Zero_nat (Suc n) = true
     1.8 -  | less_nat n Zero_nat = false
     1.9 -  | less_nat (Suc m) (Suc n) = less_nat m n;
    1.10 +fun less_nat Zero_nat (Suc n) = true;
    1.11  
    1.12 -fun minus_nat (Suc m) (Suc n) = minus_nat m n
    1.13 -  | minus_nat Zero_nat n = Zero_nat
    1.14 -  | minus_nat y Zero_nat = y;
    1.15 +fun minus_nat (Suc m) (Suc n) = minus_nat m n;
    1.16  
    1.17  end; (*struct Nat*)
    1.18  
    1.19 @@ -20,13 +16,7 @@
    1.20  struct
    1.21  
    1.22  fun pick ((k, v) :: xs) n =
    1.23 -  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
    1.24 -  | pick (x :: xs) n =
    1.25 -    let
    1.26 -      val (ka, va) = x;
    1.27 -    in
    1.28 -      (if Nat.less_nat n ka then va else pick xs (Nat.minus_nat n ka))
    1.29 -    end;
    1.30 +  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
    1.31  
    1.32  end; (*struct Codegen*)
    1.33