diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java
index 11bb6a56d..c46313ef4 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java
@@ -122,35 +122,34 @@ public NameValuePairList getNamedValues(Context ctxt)
 	{
 		NameValuePairList nvl = new NameValuePairList();
 
-		FunctionValue prefunc =
-			(predef == null) ? null : new FunctionValue(predef, null, null, null);
-
-		FunctionValue postfunc =
-			(postdef == null) ? null : new FunctionValue(postdef, null, null, null);
-
-		FunctionValue func = new FunctionValue(this, prefunc, postfunc, null);
-		func.isStatic = accessSpecifier.isStatic;;
-		func.uninstantiated = (typeParams != null);
-		nvl.add(new NameValuePair(name, func));
+		FunctionValue prefunc = null;
+		FunctionValue postfunc = null;
+		FunctionValue measurefunc = null;
 
 		if (predef != null)
 		{
-			nvl.add(new NameValuePair(predef.name, prefunc));
-			prefunc.uninstantiated = (typeParams != null);
+			NameValuePairList names = predef.getNamedValues(ctxt);
+			prefunc = names.getNamedValue(predef.name);
+			nvl.addAll(names);
 		}
 
 		if (postdef != null)
 		{
-			nvl.add(new NameValuePair(postdef.name, postfunc));
-			postfunc.uninstantiated = (typeParams != null);
+			NameValuePairList names = postdef.getNamedValues(ctxt);
+			postfunc = names.getNamedValue(postdef.name);
+			nvl.addAll(names);
 		}
 		
 		if (measureDef != null && measureDef.name.isMeasureName())
 		{
-			// Add implicit measure_* functions and any pre_measure_*s too.
-			nvl.addAll(measureDef.getNamedValues(ctxt));
+			NameValuePairList names = measureDef.getNamedValues(ctxt);
+			measurefunc = names.getNamedValue(measureDef.name);
+			nvl.addAll(names);
 		}
 
+		FunctionValue func = new FunctionValue(this, prefunc, postfunc, measurefunc, null);
+		nvl.add(new NameValuePair(name, func));
+
 		return nvl;
 	}
 
@@ -195,13 +194,8 @@ public FunctionValue getPolymorphicValue(TCTypeList argTypes, Context params, Co
 		}
 		
 		TCFunctionType ftype = (TCFunctionType)INInstantiate.instantiate(getType(), params, ctxt);
-		FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, null);
+		FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, measurefv, null);
 
-		if (measurefv != null)
-		{
-			rv.setMeasure(measurefv);
-		}
-		
 		polyfuncs.put(argTypes, rv);
 		return rv;
 	}
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitOperationDefinition.java
index 0fe5572d8..9a0beb8e3 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitOperationDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitOperationDefinition.java
@@ -102,25 +102,21 @@ public NameValuePairList getNamedValues(Context ctxt)
 		NameValuePairList nvl = new NameValuePairList();
 
 		FunctionValue prefunc =
-			(predef == null) ? null : new FunctionValue(predef, null, null, null);
+			(predef == null) ? null : new FunctionValue(predef, null, null, null, null);
 
 		FunctionValue postfunc =
-			(postdef == null) ? null : new FunctionValue(postdef, null, null, null);
+			(postdef == null) ? null : new FunctionValue(postdef, null, null, null, null);
 
 		OperationValue op = new OperationValue(this, prefunc, postfunc, statedef);
-		op.isConstructor = isConstructor;
-		op.isStatic = accessSpecifier.isStatic;
 		nvl.add(new NameValuePair(name, op));
 
 		if (predef != null)
 		{
-			prefunc.isStatic = accessSpecifier.isStatic;
 			nvl.add(new NameValuePair(predef.name, prefunc));
 		}
 
 		if (postdef != null)
 		{
-			postfunc.isStatic = accessSpecifier.isStatic;
 			nvl.add(new NameValuePair(postdef.name, postfunc));
 		}
 
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java
index 7bc9e8a74..d68470934 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java
@@ -130,39 +130,34 @@ public NameValuePairList getNamedValues(Context ctxt)
 	{
 		NameValuePairList nvl = new NameValuePairList();
 
-		FunctionValue prefunc =
-			(predef == null) ? null : new FunctionValue(predef, null, null, null);
-
-		FunctionValue postfunc =
-			(postdef == null) ? null : new FunctionValue(postdef, null, null, null);
-
-		// Note, body may be null if it is really implicit. This is caught
-		// when the function is invoked. The value is needed to implement
-		// the pre_() expression for implicit functions.
-
-		FunctionValue func = new FunctionValue(this, prefunc, postfunc, null);
-		func.isStatic = accessSpecifier.isStatic;
-		func.uninstantiated = (typeParams != null);
-		nvl.add(new NameValuePair(name, func));
+		FunctionValue prefunc = null;
+		FunctionValue postfunc = null;
+		FunctionValue measurefunc = null;
 
 		if (predef != null)
 		{
-			nvl.add(new NameValuePair(predef.name, prefunc));
-			prefunc.uninstantiated = (typeParams != null);
+			NameValuePairList names = predef.getNamedValues(ctxt);
+			prefunc = names.getNamedValue(predef.name);
+			nvl.addAll(names);
 		}
 
 		if (postdef != null)
 		{
-			nvl.add(new NameValuePair(postdef.name, postfunc));
-			postfunc.uninstantiated = (typeParams != null);
+			NameValuePairList names = postdef.getNamedValues(ctxt);
+			postfunc = names.getNamedValue(postdef.name);
+			nvl.addAll(names);
 		}
-
+		
 		if (measureDef != null && measureDef.name.isMeasureName())
 		{
-			// Add implicit measure_* functions and any pre_measure_*s too.
-			nvl.addAll(measureDef.getNamedValues(ctxt));
+			NameValuePairList names = measureDef.getNamedValues(ctxt);
+			measurefunc = names.getNamedValue(measureDef.name);
+			nvl.addAll(names);
 		}
 
+		FunctionValue func = new FunctionValue(this, prefunc, postfunc, measurefunc, null);
+		nvl.add(new NameValuePair(name, func));
+
 		return nvl;
 	}
 
@@ -207,12 +202,7 @@ public FunctionValue getPolymorphicValue(TCTypeList actualTypes, Context params,
 		}
 
 		TCFunctionType ftype = (TCFunctionType)INInstantiate.instantiate(getType(), params, ctxt);
-		FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, null);
-
-		if (measurefv != null)
-		{
-			rv.setMeasure(measurefv);
-		}
+		FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, measurefv, null);
 
 		polyfuncs.put(actualTypes, rv);
 		return rv;
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitOperationDefinition.java
index 207c093a0..fd90a1d37 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitOperationDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitOperationDefinition.java
@@ -123,29 +123,25 @@ public NameValuePairList getNamedValues(Context ctxt)
 		NameValuePairList nvl = new NameValuePairList();
 
 		FunctionValue prefunc =
-			(predef == null) ? null : new FunctionValue(predef, null, null, null);
+			(predef == null) ? null : new FunctionValue(predef, null, null, null, null);
 
 		FunctionValue postfunc =
-			(postdef == null) ? null : new FunctionValue(postdef, null, null, null);
+			(postdef == null) ? null : new FunctionValue(postdef, null, null, null, null);
 
 		// Note, body may be null if it is really implicit. This is caught
 		// when the function is invoked. The value is needed to implement
 		// the pre_() expression for implicit functions.
 
 		OperationValue op =	new OperationValue(this, prefunc, postfunc, statedef);
-		op.isConstructor = isConstructor;
-		op.isStatic = accessSpecifier.isStatic;
 		nvl.add(new NameValuePair(name, op));
 
 		if (predef != null)
 		{
-			prefunc.isStatic = accessSpecifier.isStatic;
 			nvl.add(new NameValuePair(predef.name, prefunc));
 		}
 
 		if (postdef != null)
 		{
-			postfunc.isStatic = accessSpecifier.isStatic;
 			nvl.add(new NameValuePair(postdef.name, postfunc));
 		}
 
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INStateDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INStateDefinition.java
index 97735afad..553385630 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INStateDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INStateDefinition.java
@@ -115,13 +115,13 @@ public void initState(StateContext initialContext)
 	{
 		if (invdef != null)
 		{
-			invfunc = new FunctionValue(invdef, null, null, initialContext);
+			invfunc = new FunctionValue(invdef, null, null, null, initialContext);
 			initialContext.put(name.getInvName(location), invfunc);
 		}
 
 		if (initdef != null)
 		{
-			initfunc = new FunctionValue(initdef, null, null, initialContext);
+			initfunc = new FunctionValue(initdef, null, null, null, initialContext);
 			initialContext.put(name.getInitName(location), initfunc);
 		}
 
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INTypeDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INTypeDefinition.java
index 60538b6e1..59d362b60 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INTypeDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INTypeDefinition.java
@@ -90,31 +90,31 @@ public NameValuePairList getNamedValues(Context ctxt)
 
 		if (invdef != null)
 		{
-			FunctionValue invfunc =	new FunctionValue(invdef, null, null, null);
+			FunctionValue invfunc =	new FunctionValue(invdef, null, null, null, null);
 			nvl.add(new NameValuePair(invdef.name, invfunc));
 		}
 
 		if (eqdef != null)
 		{
-			FunctionValue eqfunc =	new FunctionValue(eqdef, null, null, null);
+			FunctionValue eqfunc =	new FunctionValue(eqdef, null, null, null, null);
 			nvl.add(new NameValuePair(eqdef.name, eqfunc));
 		}
 
 		if (orddef != null)
 		{
-			FunctionValue ordfunc =	new FunctionValue(orddef, null, null, null);
+			FunctionValue ordfunc =	new FunctionValue(orddef, null, null, null, null);
 			nvl.add(new NameValuePair(orddef.name, ordfunc));
 		}
 
 		if (mindef != null)
 		{
-			FunctionValue minfunc =	new FunctionValue(mindef, null, null, null);
+			FunctionValue minfunc =	new FunctionValue(mindef, null, null, null, null);
 			nvl.add(new NameValuePair(mindef.name, minfunc));
 		}
 
 		if (maxdef != null)
 		{
-			FunctionValue maxfunc =	new FunctionValue(maxdef, null, null, null);
+			FunctionValue maxfunc =	new FunctionValue(maxdef, null, null, null, null);
 			nvl.add(new NameValuePair(maxdef.name, maxfunc));
 		}
 
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INFuncInstantiationExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INFuncInstantiationExpression.java
index 1efa6c974..eaf87ccb7 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INFuncInstantiationExpression.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INFuncInstantiationExpression.java
@@ -121,7 +121,7 @@ public Value eval(Context ctxt)
 				rv = impdef.getPolymorphicValue(argtypes, params, ctxt);
 			}
 
-    		rv.setSelf(fv.self);
+    		rv.setSelf(fv);
 			rv.uninstantiated = false;
 			return rv;
 		}
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 4e73bf093..c44008a38 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
@@ -36,7 +36,6 @@
 import com.fujitsu.vdmj.pog.SubTypeObligation;
 import com.fujitsu.vdmj.tc.definitions.TCDefinition;
 import com.fujitsu.vdmj.tc.definitions.TCExplicitFunctionDefinition;
-import com.fujitsu.vdmj.tc.lex.TCNameToken;
 import com.fujitsu.vdmj.tc.types.TCMapType;
 import com.fujitsu.vdmj.tc.types.TCType;
 import com.fujitsu.vdmj.tc.types.TCTypeList;
@@ -103,9 +102,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			}
 		}
 		
-		boolean polymorphic = type.isFunction(location) && type.getFunction().instantiated != null;
-
-		if (!type.isUnknown(location) && !polymorphic &&
+		if (!type.isUnknown(location) &&
 			(type.isFunction(location) || type.isOperation(location)))
 		{
 			TCTypeList paramTypes = type.isFunction(location) ?
@@ -113,7 +110,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			
 			String prename = root.getPreName();
 
-			if (type.isFunction(location) && (prename == null || !prename.equals("")))
+			if (type.isFunction(location) && prename != null && !prename.equals(""))
 			{
 				boolean needed = true;
 				
@@ -154,10 +151,14 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			}
 		}
 
-		if (!type.isUnknown(location) && type.isFunction(location) && !polymorphic)
+		if (!type.isUnknown(location) && type.isFunction(location))
 		{
 			if (recursive != null)	// name is a function in a recursive loop
 			{
+				/**
+				 * All of the functions in the loop will generate similar obligations,
+				 * so the "add" method eliminates any duplicates.
+				 */
 				for (PODefinitionList loop: recursive)
 				{
 					obligations.add(new RecursiveObligation(location, loop, this, ctxt));
@@ -180,16 +181,16 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 		return obligations;
 	}
 	
-	public String getMeasureApply(TCNameToken measure)
+	public String getMeasureApply(String measure)
 	{
 		return getMeasureApply(measure, true);
 	}
 	
 	/**
 	 * Create a measure application string from this apply, turning the root function
-	 * name into the measure name passed, and collapsing curried argument sets into one. 
+	 * name into the measure name passed. 
 	 */
-	private String getMeasureApply(TCNameToken measure, boolean close)
+	private String getMeasureApply(String measure, boolean close)
 	{
 		String start = null;
 		
@@ -200,19 +201,31 @@ private String getMeasureApply(TCNameToken measure, boolean close)
 		}
 		else if (root instanceof POVariableExpression)
 		{
-			start = measure.getName() + "(";
+			start = measure;
 		}
 		else if (root instanceof POFuncInstantiationExpression)
 		{
 			POFuncInstantiationExpression fie = (POFuncInstantiationExpression)root;
-			start = measure.getName() + "[" + Utils.listToString(fie.actualTypes) + "](";
+			start = measure + "[" + Utils.listToString(fie.actualTypes) + "]";
 		}
 		else
 		{
-			start = root.toString() + "(";
+			start = root.toString();
 		}
+
+		StringBuilder sb = new StringBuilder(start);
+		sb.append("(");
+		String separator = "";
 		
-		return start  + Utils.listToString(args) + (close ? ")" : ", ");
+		for (POExpression arg: args)
+		{
+			sb.append(separator);
+			sb.append(Utils.deBracketed(arg));
+			separator = ", ";
+		}
+
+		sb.append(")");
+		return sb.toString();
 	}
 
 	@Override
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POExpression.java
index 4f4f56987..a071db788 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POExpression.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POExpression.java
@@ -116,13 +116,13 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 	 * This is used during proof obligation generation. It is implemented in
 	 * the VariableExpression class.
 	 * 
-	 * null => expression is not a function.
-	 * "" => expression is a function without a precondition.
-	 * "pre_<name>" => expression is a function with a precondition.
+	 * null => expression is not a function or operation.
+	 * "" => expression is a fn/op without a precondition.
+	 * "pre_<name>" => expression is a fn/op with a precondition.
 	 */
 	public String getPreName()
 	{
-		return null;	// Not a function, by default
+		return null;	// Not a fn/op, by default
 	}
 	
 	/**
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 9386d8984..0b996bfe9 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java
@@ -39,37 +39,13 @@
 
 public class RecursiveObligation extends ProofObligation
 {
-	public RecursiveObligation(
-		POExplicitFunctionDefinition def, POApplyExpression apply, POContextStack ctxt)
-	{
-		super(apply.location, POType.RECURSIVE, ctxt);
-		int measureLexical = getLex(def.measureDef);
-
-		String lhs = getLHS(def);
-		String rhs = apply.getMeasureApply(def.measureName);
-
-		value = ctxt.getObligation(greater(measureLexical, lhs, rhs));
-	}
-
-	public RecursiveObligation(
-		POImplicitFunctionDefinition def, POApplyExpression apply, POContextStack ctxt)
-	{
-		super(def.location, POType.RECURSIVE, ctxt);
-		int measureLexical = getLex(def.measureDef);
-		
-		String lhs = getLHS(def);
-		String rhs = def.measureName.getName() + "(" + apply.args + ")";
-
-		value = ctxt.getObligation(greater(measureLexical, lhs, rhs));
-	}
-	
 	public RecursiveObligation(LexLocation location, PODefinitionList defs, POApplyExpression apply, POContextStack ctxt)
 	{
 		super(location, POType.RECURSIVE, ctxt);
 		int measureLexical = getLex(getMeasureDef(defs.get(0)));
 		
 		String lhs = getLHS(defs.get(0));
-		String rhs = getMeasureName(defs.get(1)) + "(" + apply.args + ")";
+		String rhs = apply.getMeasureApply(getMeasureName(defs.get(1)));
 
 		value = ctxt.getObligation(greater(measureLexical, lhs, rhs));
 	}
@@ -95,17 +71,12 @@ private String getLHS(PODefinition def)
 				sb.append("]");
 			}
 			
-			String sep = "";
-			sb.append("(");
-			
 			for (POPatternList plist: edef.paramPatternList)
 			{
-				 sb.append(sep);
+				 sb.append("(");
 				 sb.append(Utils.listToString(plist));
-				 sep = ", ";
+				 sb.append(")");
 			}
-
-			sb.append(")");
 		}
 		else if (def instanceof POImplicitFunctionDefinition)
 		{
@@ -185,6 +156,11 @@ private int getLex(POExplicitFunctionDefinition mdef)
 		
 		TCFunctionType ftype = (TCFunctionType) mdef.getType();
 		
+		while (ftype.result instanceof TCFunctionType)	// Skip curries
+		{
+			ftype = (TCFunctionType)ftype.result;
+		}
+		
 		if (ftype.result instanceof TCProductType)
 		{
 			TCProductType type = (TCProductType)ftype.result;
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java
index 5be045511..d189c62db 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java
@@ -343,7 +343,7 @@ public void typeCheck(Environment base, NameScope scope)
 		if (measureExp instanceof TCVariableExpression)
 		{
 			TCVariableExpression exp = (TCVariableExpression)measureExp;
-			if (base.isVDMPP()) exp.name.setTypeQualifier(getMeasureParams());
+			if (base.isVDMPP()) exp.name.setTypeQualifier(type.parameters);
 			TCDefinition def = base.findName(exp.name, scope);
 			
 			if (def instanceof TCExplicitFunctionDefinition)
@@ -381,25 +381,14 @@ else if (measureExp != null)
 	 */
 	private void setMeasureExp(Environment base, Environment local, NameScope scope)
 	{
-		TCType actual = measureExp.typeCheck(local, null, NameScope.NAMES, null);
+		TCType mexpType = measureExp.typeCheck(local, null, NameScope.NAMES, null);
 		measureName = name.getMeasureName(measureExp.location);
-		checkMeasure(measureName, actual);
-		
-		// Concatenate the parameter patterns into one list for curried measures
-		TCPatternList all = new TCPatternList();
-		
-		for (TCPatternList p: paramPatternList)
-		{
-			all.addAll(p);
-		}
-		
-		TCPatternListList cpll = new TCPatternListList();
-		cpll.add(all);
+		checkMeasure(measureName, mexpType);
 		
 		// Note that the measure_f has the precondition of the function it measures.
 		
 		TCExplicitFunctionDefinition def = new TCExplicitFunctionDefinition(null, accessSpecifier, measureName,
-				typeParams, type.getMeasureType(isCurried, actual), cpll, measureExp, precondition, null, false, null);
+				typeParams, type.getMeasureType(mexpType), paramPatternList, measureExp, precondition, null, false, null);
 
 		def.classDefinition = classDefinition;
 		def.implicitDefinitions(base);
@@ -414,7 +403,7 @@ private void setMeasureExp(Environment base, Environment local, NameScope scope)
 	 */
 	private void setMeasureDef(TCNameToken mname, Environment base, NameScope scope)
 	{
-		if (base.isVDMPP()) mname.setTypeQualifier(getMeasureParams());
+		if (base.isVDMPP()) mname.setTypeQualifier(type.parameters);
 		measureDef = (TCExplicitFunctionDefinition) base.findName(mname, scope);
 
 		if (measureDef == this)
@@ -445,19 +434,27 @@ else if (this.typeParams != null && efd.typeParams != null
 			
 			if (typeParams != null)		// Polymorphic, so compare "shape" of param signature
 			{
-				if (!mtype.parameters.toString().equals(getMeasureParams().toString()))
+				if (!mtype.parameters.toString().equals(type.parameters.toString()))
 				{
 					mname.report(3303, "Measure parameters different to function");
-					detail2(mname.getName(), mtype.parameters, "Expected", getMeasureParams());
+					detail2(mname.getName(), mtype.parameters, "Expected", type.parameters);
 				}
 			}
-			else if (!TypeComparator.compatible(mtype.parameters, getMeasureParams()))
+			else if (!TypeComparator.compatible(mtype.parameters, type.parameters))
 			{
 				mname.report(3303, "Measure parameters different to function");
-				detail2(mname.getName(), mtype.parameters, "Expected", getMeasureParams());
+				detail2(mname.getName(), mtype.parameters, "Expected", type.parameters);
 			}
-
-			checkMeasure(mname, mtype.result);
+			
+			TCType result = mtype.result;
+			
+			while (result instanceof TCFunctionType)
+			{
+				TCFunctionType fr = (TCFunctionType)result;
+				result = fr.result;
+			}
+			
+			checkMeasure(mname, result);
 		}
 	}
 
@@ -496,26 +493,6 @@ public TCType getType()
 		return type;		// NB entire "->" type, not the result
 	}
 
-	private TCTypeList getMeasureParams()
-	{
-		TCTypeList params = new TCTypeList();
-		params.addAll(type.parameters);
-		
-		if (isCurried)
-		{
-			TCType rtype = type.result;
-
-			while (rtype instanceof TCFunctionType)
-			{
-				TCFunctionType ftype = (TCFunctionType)rtype;
-				params.addAll(ftype.parameters);
-				rtype = ftype.result;
-			}
-		}
-		
-		return params;
-	}
-
 	private TCType checkParams(ListIterator<TCPatternList> plists, TCFunctionType ftype)
 	{
 		TCTypeList ptypes = ftype.parameters;
@@ -646,7 +623,7 @@ public TCDefinitionList getDefinitions()
 			defs.add(postdef);
 		}
 		
-		if (measureName != null && measureName.isMeasureName())
+		if (measureDef != null && measureName.isMeasureName())
 		{
 			defs.add(measureDef);
 		}
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java
index f0c623a96..4a1153725 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java
@@ -376,14 +376,14 @@ else if (measureExp != null)
 	 */
 	private void setMeasureExp(Environment base, Environment local, NameScope scope)
 	{
-		TCType actual = measureExp.typeCheck(local, null, NameScope.NAMES, null);
+		TCType mexpType = measureExp.typeCheck(local, null, NameScope.NAMES, null);
 		measureName = name.getMeasureName(measureExp.location);
-		checkMeasure(measureName, actual);
+		checkMeasure(measureName, mexpType);
 		
 		// Note that the measure_f has the precondition of the function it measures.
 
 		TCExplicitFunctionDefinition def = new TCExplicitFunctionDefinition(null, accessSpecifier, measureName,
-				typeParams, type.getMeasureType(false, actual), getParamPatternList(), measureExp, precondition, null, false, null);
+				typeParams, type.getMeasureType(mexpType), getParamPatternList(), measureExp, precondition, null, false, null);
 
 		def.classDefinition = classDefinition;
 		def.implicitDefinitions(base);
@@ -433,6 +433,14 @@ else if (this.typeParams != null && efd.typeParams != null
 				detail2(mname.getName(), mtype.parameters, mname.getName(), type.parameters);
 			}
 
+			TCType result = mtype.result;
+			
+			while (result instanceof TCFunctionType)
+			{
+				TCFunctionType fr = (TCFunctionType)result;
+				result = fr.result;
+			}
+			
 			checkMeasure(mname, mtype.result);
 		}
 	}
@@ -492,7 +500,7 @@ public TCDefinition findName(TCNameToken sought, NameScope scope)
 		
 		if (measureDef != null && measureDef.findName(sought, scope) != null)
 		{
-			return measureDef;
+			return measureDef.findName(sought, scope);	// eg. pre_measure_f
 		}
 
 		return null;
@@ -513,7 +521,7 @@ public TCDefinitionList getDefinitions()
 			defs.add(postdef);
 		}
 		
-		if (measureName != null && measureName.isMeasureName())
+		if (measureDef != null && measureName.isMeasureName())
 		{
 			defs.add(measureDef);
 		}
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCFunctionType.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCFunctionType.java
index 7f7f1ad5a..e6053a060 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCFunctionType.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCFunctionType.java
@@ -66,27 +66,23 @@ public TCFunctionType getPostType()
 		return type;
 	}
 
-	public TCFunctionType getMeasureType(boolean isCurried, TCType actual)
+	public TCFunctionType getMeasureType(TCType actual)
 	{
-		TCTypeList cparams = new TCTypeList();
-		cparams.addAll(parameters);
-		
-		if (isCurried)
+		if (result instanceof TCFunctionType)	// Curried
 		{
-			TCFunctionType ft = this;
-			
-			while (ft.result instanceof TCFunctionType)
-			{
-				ft = (TCFunctionType)result;
-				cparams.addAll(ft.parameters);
-			}
+			TCFunctionType fresult = (TCFunctionType)result;
+			return new TCFunctionType(location, parameters, false, fresult.getMeasureType(actual));
 		}
 		
-		// Clean the return types to be precisely nat or nat-tuple.
+		TCTypeList cparams = new TCTypeList();
+		cparams.addAll(parameters);
+		
+		// Clean the return types to be a nat or nat-tuple.
+		TCType mreturn = null;
 		
 		if (actual.isNumeric(location))
 		{
-			actual = new TCNaturalType(location);
+			mreturn = new TCNaturalType(location);
 		}
 		else if (actual.isProduct(location))
 		{
@@ -98,10 +94,14 @@ else if (actual.isProduct(location))
 				nats.add(new TCNaturalType(location));
 			}
 			
-			actual = new TCProductType(location, nats);
+			mreturn = new TCProductType(location, nats);
+		}
+		else
+		{
+			mreturn = new TCUnknownType(location);
 		}
 
-		TCFunctionType type = new TCFunctionType(location, cparams, false, actual);
+		TCFunctionType type = new TCFunctionType(location, cparams, false, mreturn);
 		type.definitions = definitions;
 		return type;
 	}
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java
index b9a971c77..d8eadea65 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java
@@ -73,53 +73,58 @@ public class FunctionValue extends Value
 	public final INExpression body;
 	public final FunctionValue precondition;
 	public final FunctionValue postcondition;
-	public Context freeVariables;
+	public final FunctionValue measure;
 	public final INClassDefinition classdef;
 
-	// Causes parameter assignments to check their invariants (if any).
-	// This is set to false for inv_() functions, which cannot check them.
-	private final boolean checkInvariants;
+	public Context freeVariables;
 
-	// Measure function value, if any
-	private TCNameToken measureName = null;
-	private FunctionValue measure = null;
 	private Map<Long, Stack<Value>> measureValues = null;
 	private Set<Long> measuringThreads = null;
 	private Set<Long> callingThreads = null;
-	private ValueList curriedArgs = null;
 	private boolean isMeasure = false;
 
-	public ObjectValue self = null;
-	public boolean isStatic = false;
+	private ObjectValue self = null;
+	private boolean isStatic = false;
 	public boolean uninstantiated = false;
 
+	/**
+	 * Private constructor used by clone and curry.
+	 * @param typeValues 
+	 */
 	private FunctionValue(LexLocation location, String name, TCFunctionType type,
-		INPatternListList paramPatternList, INExpression body,
-		FunctionValue precondition, FunctionValue postcondition,
-		Context freeVariables, boolean checkInvariants, ValueList curriedArgs,
-		TCNameToken measureName, Map<Long, Stack<Value>> measureValues, INClassDefinition classdef)
+		Context typeValues, INPatternListList paramPatternList, INExpression body,
+		FunctionValue precondition, FunctionValue postcondition, FunctionValue measure,
+		Context freeVariables, Map<Long, Stack<Value>> measureValues, INClassDefinition classdef)
 	{
 		this.location = location;
 		this.name = name;
-		this.typeValues = null;
 		this.type = type;
+		this.typeValues = typeValues;
 		this.paramPatternList = paramPatternList;
 		this.body = body;
 		this.precondition = precondition;
 		this.postcondition = postcondition;
+		this.measure = measure;
 		this.freeVariables = freeVariables;
-		this.checkInvariants = checkInvariants;
-		this.curriedArgs = curriedArgs;
 		this.classdef = classdef;
 		
-		if (Settings.measureChecks && measureName != null)
+		if (Settings.measureChecks && measure != null)
 		{
-			this.measureName = measureName;
 			this.measureValues = measureValues;	// NB. a copy of the base FunctionValue's
+			
+			measure.measuringThreads = Collections.synchronizedSet(new HashSet<Long>());
+			measure.callingThreads = Collections.synchronizedSet(new HashSet<Long>());
+			measure.isMeasure = true;
+		}
+		else
+		{
+			this.measureValues = null;
 		}
 	}
 
-	// This is used by lambda expressions - so no classdef
+	/*
+	 * This is used by lambda expressions - so no classdef, pre/post/measure
+	 */
 	public FunctionValue(LexLocation location, String name, TCFunctionType type,
 		INPatternList paramPatterns, INExpression body, Context freeVariables)
 	{
@@ -132,14 +137,21 @@ public FunctionValue(LexLocation location, String name, TCFunctionType type,
 		this.precondition = null;
 		this.postcondition = null;
 		this.freeVariables = freeVariables;
-		this.checkInvariants = true;
 		this.classdef = null;
 
 		paramPatternList.add(paramPatterns);
+
+		this.measure = null;
+		this.measureValues = null;
+		this.measuringThreads = null;
+		this.callingThreads = null;
 	}
 
+	/**
+	 * Explicit functions.
+	 */
 	public FunctionValue(INExplicitFunctionDefinition def,
-		FunctionValue precondition, FunctionValue postcondition,
+		FunctionValue precondition, FunctionValue postcondition, FunctionValue measure,
 		Context freeVariables)
 	{
 		this.location = def.location;
@@ -150,19 +162,31 @@ public FunctionValue(INExplicitFunctionDefinition def,
 		this.body = def.body;
 		this.precondition = precondition;
 		this.postcondition = postcondition;
+		this.measure = measure;
 		this.freeVariables = freeVariables;
-		this.checkInvariants = !def.isTypeInvariant;
 		this.classdef = def.classDefinition;
+		this.uninstantiated = (def.typeParams != null);
+		this.isStatic = def.accessSpecifier.isStatic;
 
-		if (Settings.measureChecks && def.measureName != null)
+		if (Settings.measureChecks && measure != null)
 		{
-			measureName = def.measureName;
-			measureValues = Collections.synchronizedMap(new HashMap<Long, Stack<Value>>());
+			this.measureValues = Collections.synchronizedMap(new HashMap<Long, Stack<Value>>());
+			
+			measure.measuringThreads = Collections.synchronizedSet(new HashSet<Long>());
+			measure.callingThreads = Collections.synchronizedSet(new HashSet<Long>());
+			measure.isMeasure = true;
+		}
+		else
+		{
+			this.measureValues = null;
 		}
 	}
 
+	/**
+	 * Implicit functions.
+	 */
 	public FunctionValue(INImplicitFunctionDefinition def,
-		FunctionValue precondition, FunctionValue postcondition,
+		FunctionValue precondition, FunctionValue postcondition, FunctionValue measure,
 		Context freeVariables)
 	{
 		this.location = def.location;
@@ -183,38 +207,56 @@ public FunctionValue(INImplicitFunctionDefinition def,
 		this.body = def.body;
 		this.precondition = precondition;
 		this.postcondition = postcondition;
+		this.measure = measure;
 		this.freeVariables = freeVariables;
-		this.checkInvariants = true;
 		this.classdef = def.classDefinition;
+		this.uninstantiated = (def.typeParams != null);
+		this.isStatic = def.accessSpecifier.isStatic;
 
-		if (Settings.measureChecks && def.measureName != null)
+		if (Settings.measureChecks && measure != null)
+		{
+			this.measureValues = Collections.synchronizedMap(new HashMap<Long, Stack<Value>>());
+			
+			measure.measuringThreads = Collections.synchronizedSet(new HashSet<Long>());
+			measure.callingThreads = Collections.synchronizedSet(new HashSet<Long>());
+			measure.isMeasure = true;
+		}
+		else
 		{
-			measureName = def.measureName;
-			measureValues = Collections.synchronizedMap(new HashMap<Long, Stack<Value>>());
+			this.measureValues = null;
 		}
 	}
 
-	public FunctionValue(INImplicitFunctionDefinition fdef,
+	/**
+	 * Polymorphic explicit functions.
+	 */
+	public FunctionValue(INExplicitFunctionDefinition fdef,
 		TCFunctionType ftype, Context argTypes, FunctionValue precondition,
-		FunctionValue postcondition, Context freeVariables)
+		FunctionValue postcondition, FunctionValue measure, Context freeVariables)
 	{
-		this(fdef, precondition, postcondition, freeVariables);
+		this(fdef, precondition, postcondition, measure, freeVariables);
 		this.typeValues = argTypes;
 		this.type = ftype;
+		this.uninstantiated = false;
 	}
 
-	public FunctionValue(INExplicitFunctionDefinition fdef,
+	/**
+	 * Polymorphic implicit functions.
+	 */
+	public FunctionValue(INImplicitFunctionDefinition fdef,
 		TCFunctionType ftype, Context argTypes, FunctionValue precondition,
-		FunctionValue postcondition, Context freeVariables)
+		FunctionValue postcondition, FunctionValue measure, Context freeVariables)
 	{
-		this(fdef, precondition, postcondition, freeVariables);
+		this(fdef, precondition, postcondition, measure, freeVariables);
 		this.typeValues = argTypes;
 		this.type = ftype;
+		this.uninstantiated = false;
 	}
 
-	// This constructor is used by IterFunctionValue and CompFunctionValue
-	// The methods which matter are overridden in those classes.
-
+	/**
+	 * This constructor is used by IterFunctionValue and CompFunctionValue
+	 * The methods which matter are overridden in those classes.
+	 */
 	public FunctionValue(LexLocation location, TCFunctionType type, String name, INClassDefinition classdef)
 	{
 		this.location = location;
@@ -226,8 +268,11 @@ public FunctionValue(LexLocation location, TCFunctionType type, String name, INC
 		this.precondition = null;
 		this.postcondition = null;
 		this.freeVariables = null;
-		this.checkInvariants = true;
 		this.classdef = classdef;
+		this.measure = null;
+		this.measureValues = null;
+		this.measuringThreads = null;
+		this.callingThreads = null;
 	}
 
 	@Override
@@ -236,11 +281,26 @@ public String toString()
 		return type.toString();
 	}
 
+	public void setSelf(FunctionValue from)
+	{
+		this.self = from.self;
+	}
+	
 	public void setSelf(ObjectValue self)
 	{
 		if (!isStatic)
 		{
 			this.self = self;
+			
+			if (precondition != null)
+			{
+				precondition.setSelf(self);
+			}
+	
+			if (postcondition != null)
+			{
+				postcondition.setSelf(self);
+			}
 	
 			if (measure != null)
 			{
@@ -248,15 +308,6 @@ public void setSelf(ObjectValue self)
 			}
 		}
 	}
-	
-	public void setMeasure(FunctionValue measure)
-	{
-		measure.measuringThreads = Collections.synchronizedSet(new HashSet<Long>());
-		measure.callingThreads = Collections.synchronizedSet(new HashSet<Long>());
-		measure.isMeasure = true;
-
-		this.measure = measure;
-	}
 
 	public Value eval(
 		LexLocation from, Value arg, Context ctxt) throws ValueException
@@ -322,13 +373,10 @@ private Value eval(
 
 			// The "old" signature of type invariant functions was inv_T: T +> bool. That means that
 			// you are passing an object of type T to the invariant, rather than the RHS of the type.
-			// This was subsequently changed, so that the signature is inv_T: nat +> bool (for T=nat).
+			// This was subsequently changed, so that the signature is inv_T: T! +> bool (for T=nat).
 			// So we can always check the types of the arguments here...
-			//
-			// Was if (checkInvariants)	// Don't even convert invariant arg values
-			{
-				pv = pv.convertTo(typeIter.next(), ctxt);
-			}
+
+			pv = pv.convertTo(typeIter.next(), ctxt);
 
 			try
 			{
@@ -396,49 +444,15 @@ private Value eval(
 				}
 			}
 
-			if (measureName != null)
+			if (measure != null)
 			{
-				if (measure == null)
-				{
-					measure = evalContext.lookup(measureName).functionValue(ctxt);
-
-					if (typeValues != null)		// Function is polymorphic, so measure copies type args
-					{
-						measure = (FunctionValue)measure.clone();
-						measure.uninstantiated = false;
-						measure.typeValues = typeValues;
-					}
-
-					measure.measuringThreads = Collections.synchronizedSet(new HashSet<Long>());
-					measure.callingThreads = Collections.synchronizedSet(new HashSet<Long>());
-					measure.isMeasure = true;
-				}
-				
-				// If this is a curried function, then the measure is called with all of the
-				// previously applied argument values, in addition to the argValues.
-				
-				ValueList measureArgs = null;
-				
-				
-				if (curriedArgs == null)
-				{
-					measureArgs = argValues;
-				}
-				else
-				{
-					measureArgs = new ValueList();
-					measureArgs.addAll(curriedArgs);	// Previous args
-					measureArgs.addAll(argValues);		// Final args
-				}
-
-				// We disable the swapping and time (RT) as measure checks should be "free".
-				Value mv;
+				Value currentMeasure;
 				
 				try
 				{
 					measure.measuringThreads.add(tid);
-					evalContext.threadState.setAtomic(true);
-					mv = measure.eval(measure.location, measureArgs, evalContext).deref();
+					evalContext.threadState.setAtomic(true);	// measure checks are "free".
+					currentMeasure = measure.eval(measure.location, argValues, evalContext).deref();
 				}
 				catch (ValueException e)
 				{
@@ -458,22 +472,26 @@ private Value eval(
 					measureValues.put(tid, stack);
 				}
 
-				if (!stack.isEmpty())
+				if (!stack.isEmpty())	// Not the first call
 				{
-					Value old = stack.peek();		// Previous value
+					Value lastMeasure = stack.peek();
 
-    				if (old != null && mv.compareTo(old) >= 0)		// Not decreasing order
+    				if (lastMeasure != null && currentMeasure.compareTo(lastMeasure) >= 0)
     				{
     					String message = "Measure failure: " +
     						name + Utils.listToString("(", argValues, ", ", ")") + ", measure " +
-    						measure.name + ", current " + mv + ", previous " + old;
+    						measure.name + ", current " + currentMeasure + ", previous " + lastMeasure;
+    					
+    					// Re-initialise measure counters etc.
+    					measureValues.clear();
+    					measure.measuringThreads.clear();
+    					measure.callingThreads.clear();
     					
-    					measure = null;	// Re-initialise counters
     					abort(4146, message, evalContext);
     				}
 				}
 
-				stack.push(mv);
+				stack.push(currentMeasure);
 			}
 
 			Value rv = null;
@@ -560,33 +578,26 @@ private Value eval(
 				{
 					newpost = postcondition.curry(evalContext);
 				}
-
-				// Curried arguments are collected so that we can invoke any measure functions
-				// once we reach the final apply that does not return a function.
 				
-				ValueList argList = new ValueList();
+				FunctionValue newmeasure = null;
 				
-				if (curriedArgs != null)
+				if (measure != null)
 				{
-					argList.addAll(curriedArgs);
+					newmeasure = measure.curry(evalContext);
 				}
-				
-				argList.addAll(argValues);
-				
+
 				if (freeVariables != null)
 				{
 					evalContext.putAll(freeVariables);	// Pass free vars along chain
 				}
 
     			FunctionValue rv = new FunctionValue(location, "curried",
-    				(TCFunctionType)type.result,
+    				(TCFunctionType)type.result, typeValues,
     				paramPatternList.subList(1, paramPatternList.size()),
-    				body, newpre, newpost, evalContext, false, argList,
-    				measureName, measureValues, classdef);
+    				body, newpre, newpost, newmeasure, evalContext,
+    				measureValues, classdef);
 
     			rv.setSelf(self);
-    			rv.typeValues = typeValues;
-
         		return rv;
 			}
 
@@ -731,13 +742,10 @@ else if (to instanceof TCUnionType)
 					TCFunctionType newType = new TCFunctionType(location, domain, true, range);
 
 					// Create a new function with restricted dom/rng
-					FunctionValue restricted = new FunctionValue(location, name, newType,
-							paramPatternList, body, precondition, postcondition,
-							freeVariables, checkInvariants, curriedArgs,
-							measureName, measureValues, classdef);
+					FunctionValue restricted = new FunctionValue(location, name, newType, typeValues,
+							paramPatternList, body, precondition, postcondition, measure,
+							freeVariables, measureValues, classdef);
 
-					restricted.typeValues = typeValues;
-					
 					if (to instanceof TCNamedType)
 					{
 						return new InvariantValue((TCNamedType)to, restricted, ctxt);
@@ -760,21 +768,17 @@ private FunctionValue curry(Context newFreeVariables)
 		// Remove first set of parameters, and set the free variables instead.
 		// And adjust the return type to be the result type (a function).
 
-		return new FunctionValue(location, name, (TCFunctionType)type.result,
+		return new FunctionValue(location, name, (TCFunctionType)type.result, typeValues,
 			paramPatternList.subList(1, paramPatternList.size()),
-			body, precondition, postcondition, newFreeVariables, false, null, null, null, classdef);
+			body, precondition, postcondition, measure, newFreeVariables, null, classdef);
 	}
 
 	@Override
 	public Object clone()
 	{
-		FunctionValue copy = new FunctionValue(location, name, type,
-			paramPatternList, body, precondition, postcondition,
-			freeVariables, checkInvariants, curriedArgs,
-			measureName, measureValues, classdef);
-
-		copy.typeValues = typeValues;
-		return copy;
+		return new FunctionValue(location, name, type, typeValues,
+			paramPatternList, body, precondition, postcondition, measure,
+			freeVariables, measureValues, classdef);
 	}
 	
 	/**
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/NameValuePairList.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/NameValuePairList.java
index 2db613ce2..9a632931a 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/values/NameValuePairList.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/NameValuePairList.java
@@ -52,6 +52,20 @@ public boolean add(NameValuePair nv)
 		return super.add(nv);
 	}
 
+	@SuppressWarnings("unchecked")
+	public <T> T getNamedValue(TCNameToken sought)
+	{
+		for (NameValuePair pair: this)
+		{
+			if (pair.name.equals(sought))
+			{
+				return (T) pair.value;
+			}
+		}
+		
+		return null;
+	}
+
 	public NameValuePairList getUpdatable(ValueListenerList listeners)
 	{
 		NameValuePairList nlist = new NameValuePairList();
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java
index a74f8fd8a..d4860c1ca 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java
@@ -116,6 +116,8 @@ public OperationValue(INExplicitOperationDefinition def,
 		this.state = state;
 		this.classdef = def.classDefinition;
 		this.isAsync = def.accessSpecifier.isAsync;
+		this.isStatic = def.accessSpecifier.isStatic;
+		this.isConstructor = def.isConstructor;
 
 		traceRT =
 			Settings.dialect == Dialect.VDM_RT &&
@@ -148,6 +150,8 @@ public OperationValue(INImplicitOperationDefinition def,
 		this.state = state;
 		this.classdef = def.classDefinition;
 		this.isAsync = def.accessSpecifier.isAsync;
+		this.isStatic = def.accessSpecifier.isStatic;
+		this.isConstructor = def.isConstructor;
 
 		traceRT =
 			Settings.dialect == Dialect.VDM_RT &&
diff --git a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java
index 3c042ebf4..6d638e77e 100644
--- a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java
+++ b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java
@@ -65,92 +65,91 @@ protected void tearDown() throws Exception
 
 	private String[] expected =
 	{
-			/* 1 */ "(forall a:T2! &\n  is_(inv_T2(a), bool))\n",
-			/* 2 */ "exists a : seq of nat1 & (a <> [])\n",
-			/* 3 */ "forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
-			/* 4 */ "After instance variable initializers (iv < 10)\n",
-			/* 5 */ "forall arg1:(int * int), arg2:seq of (int) & (exists bind1:(int * int), i:int, j:int & (arg1 = bind1) and (mk_(i, j) = bind1)) and (exists bind1:seq of (int), k:int & (arg2 = bind1) and ([k] = bind1))\n",
-			/* 6 */ "(forall mk_(i, j):(int) * (int), [k]:seq of int &\n  i in set dom m)\n",
-			/* 7 */ "(forall mk_(i, j):(int) * (int) &\n  i in set dom m)\n",
-			/* 8 */ "(let x:nat1 = 123 in\n  -1 in set dom m)\n",
-			/* 9 */ "(let x:nat1 = 123 in\n  ((m(-1) > 0) =>\n    1 in set dom m))\n",
-			/* 10 */ "(let x:nat1 = 123 in\n  (not (m(-1) > 0) =>\n    -2 in set dom m))\n",
-			/* 11 */ "(let x:nat1 = 123 in\n  (not (m(-1) > 0) =>\n    ((m(-2) > 0) =>\n      2 in set dom m)))\n",
-			/* 12 */ "(let x:nat1 = 123 in\n  (not (m(-1) > 0) =>\n    (not (m(-2) > 0) =>\n      (((x < 0) or ((x > 10) or (x = 100))) =>\n        3 in set dom m))))\n",
-			/* 13 */ "(let x:nat1 = 123 in\n  (not (m(-1) > 0) =>\n    (not (m(-2) > 0) =>\n      (not ((x < 0) or ((x > 10) or (x = 100))) =>\n        999 in set dom m))))\n",
-			/* 14 */ "(forall a:int, b:int & pre_pref(a, b) =>\n  a in set dom m)\n",
-			/* 15 */ "(forall a:int, b:int &\n  pre_prepostf(a, b) => post_prepostf(a, b, (a + b)))\n",
-			/* 16 */ "(forall mk_(a, b):(int) * (int), c:(int) * (int) &\n  is_(pre_prepostfi(mk_(a, b), c), bool))\n",
-			/* 17 */ "(forall mk_(a, b):(int) * (int), c:(int) * (int) &\n  pre_prepostfi(mk_(a, b), c) => exists r:int & post_prepostfi(mk_(a, b), c, r))\n",
-			/* 18 */ "(forall x:seq of int &\n  (exists [a]:seq1 of int & [a] = (x ^ [-999]) => let [a] = (x ^ [-999]) in\n    a in set dom m))\n",
-			/* 19 */ "(forall x:seq of int &\n  (not exists [a]:seq1 of int & [a] = (x ^ [-999]) =>\n    (exists [a, b]:seq1 of int & [a, b] = (x ^ [-999]) => let [a, b] = (x ^ [-999]) in\n      (a + b) in set dom m)))\n",
-			/* 20 */ "(forall x:seq of int &\n  (not exists [a]:seq1 of int & [a] = (x ^ [-999]) =>\n    (not exists [a, b]:seq1 of int & [a, b] = (x ^ [-999]) =>\n      (exists [a] ^ [b]:seq1 of int & [a] ^ [b] = (x ^ [-999]) => let [a] ^ [b] = (x ^ [-999]) in\n        (a + b) in set dom m))))\n",
-			/* 21 */ "(forall x:seq of int &\n  (not exists [a]:seq1 of int & [a] = (x ^ [-999]) =>\n    (not exists [a, b]:seq1 of int & [a, b] = (x ^ [-999]) =>\n      (not exists [a] ^ [b]:seq1 of int & [a] ^ [b] = (x ^ [-999]) =>\n        m(999) in set dom m))))\n",
-			/* 22 */ "(forall x:seq of int &\n  (not exists [a]:seq1 of int & [a] = (x ^ [-999]) =>\n    (not exists [a, b]:seq1 of int & [a, b] = (x ^ [-999]) =>\n      (not exists [a] ^ [b]:seq1 of int & [a] ^ [b] = (x ^ [-999]) =>\n        999 in set dom m))))\n",
-			/* 23 */ "(forall mk_(i, $any1):(int) * (int) &\n  exists x in set {m(1), 2, 3} & (m(x) < i))\n",
-			/* 24 */ "(forall mk_(i, $any1):(int) * (int) &\n  1 in set dom m)\n",
-			/* 25 */ "(forall mk_(i, $any1):(int) * (int) &\n  (forall x in set {m(1), 2, 3} &\n    x in set dom m))\n",
-			/* 26 */ "(forall mk_(i, $any1):(int) * (int) &\n  (forall x in set {m(1), 2, 3} & (m(x) < i) =>\n    x in set dom m))\n",
-			/* 27 */ "(let x:int = m(1) in\n  1 in set dom m)\n",
-			/* 28 */ "(let x:int = m(1) in\n  x in set dom m)\n",
-			/* 29 */ "(let local: int -> int local(x) == m(x) in\n  (forall x:int &\n    x in set dom m))\n",
-			/* 30 */ "(let x = m(1) in\n  1 in set dom m)\n",
-			/* 31 */ "(let x = m(1) in\n  (let y = m(2) in\n    2 in set dom m))\n",
-			/* 32 */ "(let x = m(1), y = m(2) in\n  x in set dom m)\n",
-			/* 33 */ "(let x = m(1), y = m(2) in\n  y in set dom m)\n",
-			/* 34 */ "exists1 x in set {1, 2, 3} & (x < 10)\n",
-			/* 35 */ "(forall n:nat &\n  n > 1 => forall arg:nat & pre_f1(arg) => pre_f1(f1(arg)))\n",
-			/* 36 */ "(forall x:int -> int, n:nat &\n  n > 1 => forall arg:nat & pre_(x, arg) => pre_(x, x(arg)))\n",
-			/* 37 */ "(forall n:nat &\n  n = 0 or n = 1 or rng(m) subset dom(m))\n",
-			/* 38 */ "(forall x:map int to int, n:nat &\n  n = 0 or n = 1 or rng(x) subset dom(x))\n",
-			/* 39 */ "forall arg:int & pre_f2(arg) => pre_f1(f2(arg))\n",
-			/* 40 */ "(forall x:int -> int, y:int -> int &\n  forall arg:int & pre_(y, arg) => pre_(x, y(arg)))\n",
-			/* 41 */ "(forall x:int -> int &\n  forall arg:int & pre_f2(arg) => pre_(x, f2(arg)))\n",
-			/* 42 */ "(forall x:int -> int &\n  forall arg:int & pre_(x, arg) => pre_f1(x(arg)))\n",
-			/* 43 */ "rng(m) subset dom(m)\n",
-			/* 44 */ "(forall x:map int to int, y:map int to int &\n  rng(y) subset dom(x))\n",
-			/* 45 */ "(forall x:map int to int &\n  rng(m) subset dom(x))\n",
-			/* 46 */ "(forall i:int &\n  pre_f1(i))\n",
-			/* 47 */ "(forall x:int -> int &\n  pre_(x, 123))\n",
-			/* 48 */ "(forall i:int &\n  i in set inds sq)\n",
-			/* 49 */ "(forall x:seq of int &\n  123 in set inds x)\n",
-			/* 50 */ "(forall s:set of (set of int) &\n  s <> {})\n",
-			/* 51 */ "(forall s:seq of int &\n  (not (s = []) =>\n    s <> []))\n",
-			/* 52 */ "(forall i:int &\n  i <> 0)\n",
-			/* 53 */ "(forall i:int &\n  is_int((123 / i)))\n",
-			/* 54 */ "(forall i:int &\n  i <> 0)\n",
-			/* 55 */ "exists finmap1:map nat to (map int to nat1) & forall a:int, b in set {1, 2, 3} & (a < 10) => exists findex2 in set dom finmap1 & finmap1(findex2) = {a |-> b}\n",
-			/* 56 */ "exists finmap1:map nat to (int) & forall a:int, b in set {1, 2, 3} & (a < 10) => exists findex2 in set dom finmap1 & finmap1(findex2) = (a + b)\n",
-			/* 57 */ "(forall a:map int to int, b:map int to int &\n  forall ldom1 in set dom a, rdom2 in set dom b & ldom1 = rdom2 => a(ldom1) = b(rdom2))\n",
-			/* 58 */ "(forall x:int &\n  forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}, {x |-> 4}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4))\n",
-			/* 59 */ "forall m1 in set {{1 |-> 2}, {2 |-> 3}}, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
-			/* 60 */ "(forall n:nat &\n  is_(measure_recursive(n), nat))\n",
-			/* 61 */ "(forall n:nat &\n  (not (n = 1) =>\n    (n - 1) >= 0))\n",
-			/* 62 */ "(forall n:nat &\n  (not (n = 1) =>\n    measure_recursive(n) > measure_recursive((n - 1))))\n",
-			/* 63 */ "dom {1 |-> false} subset inds [2, true, 7.8]\n",
-			/* 64 */ "is_(([2, true, 7.8] ++ {1 |-> false}), seq of (bool | nat))\n",
-			/* 65 */ "(forall t:((nat) * (nat) * (nat)) | ((nat) * (nat)) &\n  is_(t, (nat) * (nat) * (nat)))\n",
-			/* 66 */ "(forall u:U &\n  (let mk_(a, b):U = u in\n    exists mk_(a, b):U & mk_(a, b) = u))\n",
-			/* 67 */ "(forall u:U &\n  (let mk_(a, b):U = u in\n    is_(u, (nat) * (nat))))\n",
-			/* 68 */ "(is_([1, 2, true], T1) and ((is_(1, bool)) and (is_(2, bool)))) or (is_([1, 2, true], T2) and inv_T2([1, 2, true]))\n",
-			/* 69 */ "(forall t:T1 | T2 &\n  (let x:T1 | T2 = [1, 2, 3, true] in\n    (is_([1, 2, 3, true], T1) and ((is_(1, bool)) and (is_(2, bool)) and (is_(3, bool)))) or (is_([1, 2, 3, true], T2) and inv_T2([1, 2, 3, true]))))\n",
-			/* 70 */ "(forall a:T1 | T2 | int &\n  (is_(a, T1) and (is_(a, seq of bool))) or (is_(a, T2) and inv_T2(a)))\n",
-			/* 71 */ "is_({1 |-> \"2\"}, inmap nat1 to seq1 of char)\n",
-			/* 72 */ "(forall n:nat1, x:nat1 &\n  (not (n < 2) =>\n    (n - 1) > 0))\n",
-			/* 73 */ "(forall n:nat1, x:nat1 &\n  (not (n < 2) =>\n    (x - 1) > 0))\n",
-			/* 74 */ "(forall n:nat1, x:nat1 &\n  (not (n < 2) =>\n    id(n, x) > id((n - 1), (x - 1))))\n",
-			/* 75 */ "(forall x:nat1, y:nat1 &\n  (x - y) >= 0)\n",
-			/* 76 */ "(forall mk_(n, x):(nat1) * (nat1) &\n  (not (n < 2) =>\n    ((n - 1) > 0) and ((x - 1) > 0)))\n",
-			/* 77 */ "(forall mk_(n, x):(nat1) * (nat1) &\n  (not (n < 2) =>\n    id2(mk_(n, x)) > id2(mk_((n - 1), (x - 1)))))\n",
-			/* 78 */ "(forall mk_(x, y):(nat1) * (nat1) &\n  (x - y) >= 0)\n",
-			/* 79 */ "(forall mk_(n, x):(nat1) * (nat1) &\n  (not (n < 2) =>\n    ((n - 1) > 0) and ((x - 1) > 0)))\n",
-			/* 80 */ "(forall mk_(n, x):(nat1) * (nat1) &\n  (not (n < 2) =>\n    (let lhs = id3(mk_(n, x)), rhs = id3(mk_((n - 1), (x - 1))) in if lhs.#1 <> rhs.#1 then lhs.#1 > rhs.#1 else lhs.#2 > rhs.#2)))\n",
-			/* 81 */ "1 in set dom m\n",
-			/* 82 */ "1 in set dom m\n",
-			/* 83 */ "2 in set dom m\n",
-			/* 84 */ "3 in set dom m\n",
-			/* 85 */ "while (x > 0) do ...\n",
-			/* 86 */ "After iv := (iv + 1) (iv < 10)\n"
+		/* 1 */ "(forall a:T2! &\n  is_(inv_T2(a), bool))\n",
+		/* 2 */ "exists a : seq of nat1 & (a <> [])\n",
+		/* 3 */ "forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
+		/* 4 */ "After instance variable initializers (iv < 10)\n",
+		/* 5 */ "forall arg1:(int * int), arg2:seq of (int) & (exists bind1:(int * int), i:int, j:int & (arg1 = bind1) and (mk_(i, j) = bind1)) and (exists bind1:seq of (int), k:int & (arg2 = bind1) and ([k] = bind1))\n",
+		/* 6 */ "(forall mk_(i, j):(int) * (int), [k]:seq of int &\n  i in set dom m)\n",
+		/* 7 */ "(forall mk_(i, j):(int) * (int) &\n  i in set dom m)\n",
+		/* 8 */ "(let x:nat1 = 123 in\n  -1 in set dom m)\n",
+		/* 9 */ "(let x:nat1 = 123 in\n  ((m(-1) > 0) =>\n    1 in set dom m))\n",
+		/* 10 */ "(let x:nat1 = 123 in\n  (not (m(-1) > 0) =>\n    -2 in set dom m))\n",
+		/* 11 */ "(let x:nat1 = 123 in\n  (not (m(-1) > 0) =>\n    ((m(-2) > 0) =>\n      2 in set dom m)))\n",
+		/* 12 */ "(let x:nat1 = 123 in\n  (not (m(-1) > 0) =>\n    (not (m(-2) > 0) =>\n      (((x < 0) or ((x > 10) or (x = 100))) =>\n        3 in set dom m))))\n",
+		/* 13 */ "(let x:nat1 = 123 in\n  (not (m(-1) > 0) =>\n    (not (m(-2) > 0) =>\n      (not ((x < 0) or ((x > 10) or (x = 100))) =>\n        999 in set dom m))))\n",
+		/* 14 */ "(forall a:int, b:int & pre_pref(a, b) =>\n  a in set dom m)\n",
+		/* 15 */ "(forall a:int, b:int &\n  pre_prepostf(a, b) => post_prepostf(a, b, (a + b)))\n",
+		/* 16 */ "(forall mk_(a, b):(int) * (int), c:(int) * (int) &\n  is_(pre_prepostfi(mk_(a, b), c), bool))\n",
+		/* 17 */ "(forall mk_(a, b):(int) * (int), c:(int) * (int) &\n  pre_prepostfi(mk_(a, b), c) => exists r:int & post_prepostfi(mk_(a, b), c, r))\n",
+		/* 18 */ "(forall x:seq of int &\n  (exists [a]:seq1 of int & [a] = (x ^ [-999]) => let [a] = (x ^ [-999]) in\n    a in set dom m))\n",
+		/* 19 */ "(forall x:seq of int &\n  (not exists [a]:seq1 of int & [a] = (x ^ [-999]) =>\n    (exists [a, b]:seq1 of int & [a, b] = (x ^ [-999]) => let [a, b] = (x ^ [-999]) in\n      (a + b) in set dom m)))\n",
+		/* 20 */ "(forall x:seq of int &\n  (not exists [a]:seq1 of int & [a] = (x ^ [-999]) =>\n    (not exists [a, b]:seq1 of int & [a, b] = (x ^ [-999]) =>\n      (exists [a] ^ [b]:seq1 of int & [a] ^ [b] = (x ^ [-999]) => let [a] ^ [b] = (x ^ [-999]) in\n        (a + b) in set dom m))))\n",
+		/* 21 */ "(forall x:seq of int &\n  (not exists [a]:seq1 of int & [a] = (x ^ [-999]) =>\n    (not exists [a, b]:seq1 of int & [a, b] = (x ^ [-999]) =>\n      (not exists [a] ^ [b]:seq1 of int & [a] ^ [b] = (x ^ [-999]) =>\n        m(999) in set dom m))))\n",
+		/* 22 */ "(forall x:seq of int &\n  (not exists [a]:seq1 of int & [a] = (x ^ [-999]) =>\n    (not exists [a, b]:seq1 of int & [a, b] = (x ^ [-999]) =>\n      (not exists [a] ^ [b]:seq1 of int & [a] ^ [b] = (x ^ [-999]) =>\n        999 in set dom m))))\n",
+		/* 23 */ "(forall mk_(i, $any1):(int) * (int) &\n  exists x in set {m(1), 2, 3} & (m(x) < i))\n",
+		/* 24 */ "(forall mk_(i, $any1):(int) * (int) &\n  1 in set dom m)\n",
+		/* 25 */ "(forall mk_(i, $any1):(int) * (int) &\n  (forall x in set {m(1), 2, 3} &\n    x in set dom m))\n",
+		/* 26 */ "(forall mk_(i, $any1):(int) * (int) &\n  (forall x in set {m(1), 2, 3} & (m(x) < i) =>\n    x in set dom m))\n",
+		/* 27 */ "(let x:int = m(1) in\n  1 in set dom m)\n",
+		/* 28 */ "(let x:int = m(1) in\n  x in set dom m)\n",
+		/* 29 */ "(let local: int -> int local(x) == m(x) in\n  (forall x:int &\n    x in set dom m))\n",
+		/* 30 */ "(let x = m(1) in\n  1 in set dom m)\n",
+		/* 31 */ "(let x = m(1) in\n  (let y = m(2) in\n    2 in set dom m))\n",
+		/* 32 */ "(let x = m(1), y = m(2) in\n  x in set dom m)\n",
+		/* 33 */ "(let x = m(1), y = m(2) in\n  y in set dom m)\n",
+		/* 34 */ "exists1 x in set {1, 2, 3} & (x < 10)\n",
+		/* 35 */ "(forall n:nat &\n  n > 1 => forall arg:nat & pre_f1(arg) => pre_f1(f1(arg)))\n",
+		/* 36 */ "(forall x:int -> int, n:nat &\n  n > 1 => forall arg:nat & pre_(x, arg) => pre_(x, x(arg)))\n",
+		/* 37 */ "(forall n:nat &\n  n = 0 or n = 1 or rng(m) subset dom(m))\n",
+		/* 38 */ "(forall x:map int to int, n:nat &\n  n = 0 or n = 1 or rng(x) subset dom(x))\n",
+		/* 39 */ "forall arg:int & pre_f2(arg) => pre_f1(f2(arg))\n",
+		/* 40 */ "(forall x:int -> int, y:int -> int &\n  forall arg:int & pre_(y, arg) => pre_(x, y(arg)))\n",
+		/* 41 */ "(forall x:int -> int &\n  forall arg:int & pre_f2(arg) => pre_(x, f2(arg)))\n",
+		/* 42 */ "(forall x:int -> int &\n  forall arg:int & pre_(x, arg) => pre_f1(x(arg)))\n",
+		/* 43 */ "rng(m) subset dom(m)\n",
+		/* 44 */ "(forall x:map int to int, y:map int to int &\n  rng(y) subset dom(x))\n",
+		/* 45 */ "(forall x:map int to int &\n  rng(m) subset dom(x))\n",
+		/* 46 */ "(forall i:int &\n  pre_f1(i))\n",
+		/* 47 */ "(forall i:int &\n  i in set inds sq)\n",
+		/* 48 */ "(forall x:seq of int &\n  123 in set inds x)\n",
+		/* 49 */ "(forall s:set of (set of int) &\n  s <> {})\n",
+		/* 50 */ "(forall s:seq of int &\n  (not (s = []) =>\n    s <> []))\n",
+		/* 51 */ "(forall i:int &\n  i <> 0)\n",
+		/* 52 */ "(forall i:int &\n  is_int((123 / i)))\n",
+		/* 53 */ "(forall i:int &\n  i <> 0)\n",
+		/* 54 */ "exists finmap1:map nat to (map int to nat1) & forall a:int, b in set {1, 2, 3} & (a < 10) => exists findex2 in set dom finmap1 & finmap1(findex2) = {a |-> b}\n",
+		/* 55 */ "exists finmap1:map nat to (int) & forall a:int, b in set {1, 2, 3} & (a < 10) => exists findex2 in set dom finmap1 & finmap1(findex2) = (a + b)\n",
+		/* 56 */ "(forall a:map int to int, b:map int to int &\n  forall ldom1 in set dom a, rdom2 in set dom b & ldom1 = rdom2 => a(ldom1) = b(rdom2))\n",
+		/* 57 */ "(forall x:int &\n  forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}, {x |-> 4}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4))\n",
+		/* 58 */ "forall m1 in set {{1 |-> 2}, {2 |-> 3}}, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
+		/* 59 */ "(forall n:nat &\n  is_(measure_recursive(n), nat))\n",
+		/* 60 */ "(forall n:nat &\n  (not (n = 1) =>\n    (n - 1) >= 0))\n",
+		/* 61 */ "(forall n:nat &\n  (not (n = 1) =>\n    measure_recursive(n) > measure_recursive(n - 1)))\n",
+		/* 62 */ "dom {1 |-> false} subset inds [2, true, 7.8]\n",
+		/* 63 */ "is_(([2, true, 7.8] ++ {1 |-> false}), seq of (bool | nat))\n",
+		/* 64 */ "(forall t:((nat) * (nat) * (nat)) | ((nat) * (nat)) &\n  is_(t, (nat) * (nat) * (nat)))\n",
+		/* 65 */ "(forall u:U &\n  (let mk_(a, b):U = u in\n    exists mk_(a, b):U & mk_(a, b) = u))\n",
+		/* 66 */ "(forall u:U &\n  (let mk_(a, b):U = u in\n    is_(u, (nat) * (nat))))\n",
+		/* 67 */ "(is_([1, 2, true], T1) and ((is_(1, bool)) and (is_(2, bool)))) or (is_([1, 2, true], T2) and inv_T2([1, 2, true]))\n",
+		/* 68 */ "(forall t:T1 | T2 &\n  (let x:T1 | T2 = [1, 2, 3, true] in\n    (is_([1, 2, 3, true], T1) and ((is_(1, bool)) and (is_(2, bool)) and (is_(3, bool)))) or (is_([1, 2, 3, true], T2) and inv_T2([1, 2, 3, true]))))\n",
+		/* 69 */ "(forall a:T1 | T2 | int &\n  (is_(a, T1) and (is_(a, seq of bool))) or (is_(a, T2) and inv_T2(a)))\n",
+		/* 70 */ "is_({1 |-> \"2\"}, inmap nat1 to seq1 of char)\n",
+		/* 71 */ "(forall n:nat1, x:nat1 &\n  (not (n < 2) =>\n    (n - 1) > 0))\n",
+		/* 72 */ "(forall n:nat1, x:nat1 &\n  (not (n < 2) =>\n    (x - 1) > 0))\n",
+		/* 73 */ "(forall n:nat1, x:nat1 &\n  (not (n < 2) =>\n    id(n, x) > id(n - 1, x - 1)))\n",
+		/* 74 */ "(forall x:nat1, y:nat1 &\n  (x - y) >= 0)\n",
+		/* 75 */ "(forall mk_(n, x):(nat1) * (nat1) &\n  (not (n < 2) =>\n    ((n - 1) > 0) and ((x - 1) > 0)))\n",
+		/* 76 */ "(forall mk_(n, x):(nat1) * (nat1) &\n  (not (n < 2) =>\n    id2(mk_(n, x)) > id2(mk_((n - 1), (x - 1)))))\n",
+		/* 77 */ "(forall mk_(x, y):(nat1) * (nat1) &\n  (x - y) >= 0)\n",
+		/* 78 */ "(forall mk_(n, x):(nat1) * (nat1) &\n  (not (n < 2) =>\n    ((n - 1) > 0) and ((x - 1) > 0)))\n",
+		/* 79 */ "(forall mk_(n, x):(nat1) * (nat1) &\n  (not (n < 2) =>\n    (let lhs = id3(mk_(n, x)), rhs = id3(mk_((n - 1), (x - 1))) in if lhs.#1 <> rhs.#1 then lhs.#1 > rhs.#1 else lhs.#2 > rhs.#2)))\n",
+		/* 80 */ "1 in set dom m\n",
+		/* 81 */ "1 in set dom m\n",
+		/* 82 */ "2 in set dom m\n",
+		/* 83 */ "3 in set dom m\n",
+		/* 84 */ "while (x > 0) do ...\n",
+		/* 85 */ "After iv := (iv + 1) (iv < 10)\n"
 	};
 
 	public void testPOG() throws Exception
diff --git a/vdmj/src/test/resources/Overture/evaluate/curried.vpp b/vdmj/src/test/resources/Overture/evaluate/curried.vpp
index acab87b86..059f468f4 100644
--- a/vdmj/src/test/resources/Overture/evaluate/curried.vpp
+++ b/vdmj/src/test/resources/Overture/evaluate/curried.vpp
@@ -7,8 +7,8 @@ functions
 		else curry(a1, a2)(b-1)
 	measure mc;
 	
-	mc: nat * nat * nat -> nat
-	mc(-, -, c) == c;
+	mc: nat * nat -> nat -> nat
+	mc(-, -)(c) == c;
 	
 	public fact(a: nat) r:nat ==
 		if a = 1 then 1 else a * fact(a-1)
@@ -27,8 +27,8 @@ functions
 		else [f(hd l)]^(fmap[@elem](f)(tl l))
 	measure mfmap;
 	
-	mfmap[@elem]: (@elem -> @elem) * seq of @elem -> nat
-	mfmap(-, s) == len s;
+	mfmap[@elem]: (@elem -> @elem) -> seq of @elem -> nat
+	mfmap(-)(s) == len s;
 	
 	public poly[@T]: seq of @T -> nat
 	poly(a) ==