author | bulwahn |
Tue, 13 Jul 2010 18:01:42 +0200 | |
changeset 37808 | e604e5f9bb6a |
parent 37807 | 3dc7008e750f |
child 37810 | 4270d4b0284a |
--- a/src/HOL/Product_Type.thy Tue Jul 13 16:30:13 2010 +0200 +++ b/src/HOL/Product_Type.thy Tue Jul 13 18:01:42 2010 +0200 @@ -289,7 +289,7 @@ fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y; *} attach (test) {* -fun term_of_prod aG aT bG bT i = +fun gen_prod aG aT bG bT i = let val (x, t) = aG i; val (y, u) = bG i