src/HOL/Product_Type.thy
changeset 25885 6fbc3f54f819
parent 25534 d0b74fdd6067
child 26143 314c0bcb7df7
     1.1 --- a/src/HOL/Product_Type.thy	Thu Jan 10 17:06:41 2008 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Jan 10 19:09:21 2008 +0100
     1.3 @@ -941,10 +941,14 @@
     1.4  types_code
     1.5    "*"     ("(_ */ _)")
     1.6  attach (term_of) {*
     1.7 -fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
     1.8 +fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
     1.9  *}
    1.10  attach (test) {*
    1.11 -fun gen_id_42 aG bG i = (aG i, bG i);
    1.12 +fun gen_id_42 aG aT bG bT i =
    1.13 +  let
    1.14 +    val (x, t) = aG i;
    1.15 +    val (y, u) = bG i
    1.16 +  in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end;
    1.17  *}
    1.18  
    1.19  consts_code