correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)
authorbulwahn
Tue Jul 13 18:01:42 2010 +0200 (2010-07-13)
changeset 37808e604e5f9bb6a
parent 37807 3dc7008e750f
child 37810 4270d4b0284a
correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Tue Jul 13 16:30:13 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Jul 13 18:01:42 2010 +0200
     1.3 @@ -289,7 +289,7 @@
     1.4  fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
     1.5  *}
     1.6  attach (test) {*
     1.7 -fun term_of_prod aG aT bG bT i =
     1.8 +fun gen_prod aG aT bG bT i =
     1.9    let
    1.10      val (x, t) = aG i;
    1.11      val (y, u) = bG i