diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java
index 69762ff46..843d9b829 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java
@@ -29,6 +29,7 @@
 import com.fujitsu.vdmj.po.statements.POClassInvariantStatement;
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.POGState;
+import com.fujitsu.vdmj.pog.PONameContext;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.tc.definitions.TCClassDefinition;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
@@ -183,7 +184,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 
 		for (PODefinition def: definitions)
 		{
-			list.addAll(def.getProofObligations(new POContextStack(), new POGState(), local));
+			ctxt.push(new PONameContext(def.getVariableNames()));
+			list.addAll(def.getProofObligations(ctxt, new POGState(), local));
+			ctxt.pop();
 		}
 		
 		list.typeCheck(tcdef.name, local);