doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
changeset 25056 743f3603ba8b
parent 24421 acfb2413faa3
child 26318 967323f93c67
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Tue Oct 16 17:06:21 2007 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Tue Oct 16 17:07:40 2007 +0200
     1.3 @@ -19,9 +19,14 @@
     1.4    | minus_nat Zero_nat n = Zero_nat
     1.5    | minus_nat m Zero_nat = m;
     1.6  
     1.7 -fun prod_case f1 (a, b) = f1 a b;
     1.8 +end; (*struct Nat*)
     1.9  
    1.10 -end; (*struct Nat*)
    1.11 +structure Product_Type = 
    1.12 +struct
    1.13 +
    1.14 +fun split c (a, b) = c a b;
    1.15 +
    1.16 +end; (*struct Product_Type*)
    1.17  
    1.18  structure Codegen = 
    1.19  struct
    1.20 @@ -30,7 +35,8 @@
    1.21    (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
    1.22    | pick (x :: xs) n =
    1.23      let
    1.24 -      val (k, v) = x;
    1.25 +      val a = x;
    1.26 +      val (k, v) = a;
    1.27      in
    1.28        (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
    1.29      end;