diff -r 2e9bf718a7a1 -r 65631ca437c9 src/ZF/Tools/datatype_package.ML --- 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