1 files changed, 20 insertions, 1 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 5e69bce8..54de4905 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1509,7 +1509,26 @@ namespace Microsoft.Dafny {
           PrintExpression(e.Value, false);
           wr.Write("]");
           if (parensNeeded) { wr.Write(")"); }
-        }
+        }
+
+      } else if (expr is DatatypeUpdateExpr) {
+        var e = (DatatypeUpdateExpr)expr;
+        // determine if parens are needed
+        int opBindingStrength = 0x70;
+        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+        if (parensNeeded) { wr.Write("("); }
+        PrintExpr(e.Root, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);
+        wr.Write(".(");
+        var sep = "";
+        foreach (var update in e.Updates) {
+          wr.Write("{0}{1} := ", sep, update.Item2);
+          PrintExpression(update.Item3, false);
+          sep = ", ";
+        }
+        wr.Write(")");
+        if (parensNeeded) { wr.Write(")"); }
+
       } else if (expr is ApplyExpr) {
         var e = (ApplyExpr)expr;
         // determine if parens are needed