diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java
index 18cb40d75..f7ab33fba 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java
@@ -96,7 +96,10 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 		{
 			if (type.isOperation(location))
 			{
-				pogState.addOperation(location, opdef);
+				// We have to say that the POGState is as if the operation updates state, because
+				// it may read state even if pure, and an apply uses the return value. So QC can't
+				// evaluate them. This makes subsequent POs Unchecked.
+				pogState.setUpdateState(true, location);
 			}
 
 			if (type.isMap(location))
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java
index b01c20bfb..c44a693d0 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java
@@ -30,12 +30,12 @@
 import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition;
 import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition;
 import com.fujitsu.vdmj.po.expressions.POApplyExpression;
+import com.fujitsu.vdmj.po.patterns.POPattern;
 import com.fujitsu.vdmj.po.patterns.POPatternList;
 import com.fujitsu.vdmj.po.types.POPatternListTypePair;
 import com.fujitsu.vdmj.tc.types.TCFunctionType;
 import com.fujitsu.vdmj.tc.types.TCProductType;
 import com.fujitsu.vdmj.tc.types.TCType;
-import com.fujitsu.vdmj.util.Utils;
 
 public class RecursiveObligation extends ProofObligation
 {
@@ -81,9 +81,17 @@ private String getLHS(PODefinition def)
 			
 			for (POPatternList plist: edef.paramPatternList)
 			{
-				 sb.append("(");
-				 sb.append(Utils.listToString(plist));
-				 sb.append(")");
+				String sep = "";
+				sb.append("(");
+
+				for (POPattern p: plist)
+				{
+					sb.append(sep);
+					sb.append(p.removeIgnorePatterns());
+					sep = ", ";
+				}
+
+				sb.append(")");
 			}
 		}
 		else if (def instanceof POImplicitFunctionDefinition)