changeset 41310 | 65631ca437c9 |
parent 39557 | fe5722fce758 |
child 42290 | b1f544c84040 |
--- a/src/ZF/Tools/datatype_package.ML Mon Dec 20 15:24:25 2010 +0100 +++ b/src/ZF/Tools/datatype_package.ML Mon Dec 20 16:44:33 2010 +0100 @@ -91,7 +91,7 @@ (** Define the constructors **) (*The empty tuple is 0*) - fun mk_tuple [] = @{const "0"} + fun mk_tuple [] = @{const zero} | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; fun mk_inject n k u = Balanced_Tree.access