diff --git a/tlatools/src/tlc2/value/IValue.java b/tlatools/src/tlc2/value/IValue.java
index c9681542363c9d6928dc5ede8b36898ea5939eec..30e7a4addfc2052935bc77e8b80301130db20f94 100644
--- a/tlatools/src/tlc2/value/IValue.java
+++ b/tlatools/src/tlc2/value/IValue.java
@@ -119,6 +119,8 @@ public interface IValue extends Comparable<Object> {
 
 	String toString(String delim);
 	
+	String toUnquotedString();
+
 	default boolean isAtom() {
 		if (this instanceof ModelValue || this instanceof IntValue || this instanceof StringValue
 				|| this instanceof BoolValue) {
@@ -133,4 +135,5 @@ public interface IValue extends Comparable<Object> {
 	default boolean mutates() {
 		return true;
 	}
+
 }
\ No newline at end of file
diff --git a/tlatools/src/tlc2/value/impl/StringValue.java b/tlatools/src/tlc2/value/impl/StringValue.java
index 38b4dd0903ada93e786e2e34dc2b2e11d89acbf8..5e3e203210b58749e2dcdd9d2466cdb83c255590 100644
--- a/tlatools/src/tlc2/value/impl/StringValue.java
+++ b/tlatools/src/tlc2/value/impl/StringValue.java
@@ -280,6 +280,12 @@ public class StringValue extends Value {
     }
   }
 
+  /* Same as toString. */
+  @Override
+  public final String toUnquotedString() {
+	  return PrintVersion(this.val.toString());
+  }
+
 	public static IValue createFrom(final IValueInputStream vos) throws IOException {
 		final UniqueString str = UniqueString.read(vos.getInputStream());
 		final IValue res = new StringValue(str);
diff --git a/tlatools/src/tlc2/value/impl/Value.java b/tlatools/src/tlc2/value/impl/Value.java
index ab6741f63b9cc6efb5c81381f5556c906d6473af..f03c21f96746dc397b644a44fd5f03c6a2cb6672 100644
--- a/tlatools/src/tlc2/value/impl/Value.java
+++ b/tlatools/src/tlc2/value/impl/Value.java
@@ -316,6 +316,12 @@ public abstract class Value implements ValueConstants, Serializable, IValue {
 	  return toStringImpl("", false);
   }
 
+  /* Same as toString. */
+  @Override
+  public String toUnquotedString() {
+	  return toString();
+  }
+
   @Override
   public final String toString(final String delim) {
 	  return toStringImpl(delim, true);