diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java
index ef644f876..0a9c64bbc 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java
@@ -56,7 +56,24 @@ public String toString()
 	@Override
 	public String toSource()
 	{
-		return "mk_" + typename + "(" + Utils.listToString(plist) + ")";
+		StringBuilder sb = new StringBuilder();
+		
+		sb.append("mk_");
+		sb.append(typename);
+		sb.append("(");
+		
+		String sep = "";
+		
+		for (TCPattern p: plist)
+		{
+			sb.append(sep);
+			sb.append(p.toSource());
+			sep =", ";
+		}
+		
+		sb.append(")");
+		
+		return sb.toString();
 	}
 
 	@Override