src/ZF/Tools/datatype_package.ML
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