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 0a9c64bbc..8b289f18a 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
@@ -26,6 +26,7 @@
 
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
 import com.fujitsu.vdmj.tc.patterns.visitors.TCPatternVisitor;
+import com.fujitsu.vdmj.tc.types.TCRecordType;
 import com.fujitsu.vdmj.tc.types.TCType;
 import com.fujitsu.vdmj.tc.types.TCUnresolvedType;
 import com.fujitsu.vdmj.typechecker.Environment;
@@ -92,6 +93,16 @@ public void typeResolve(Environment env)
 		{
 			plist.typeResolve(env);
 			type = type.typeResolve(env);
+			
+			if (type instanceof TCRecordType)
+			{
+				TCRecordType recordType = (TCRecordType)type;
+				
+				if (recordType.opaque && !location.module.equals(recordType.location.module))
+				{
+					report(3127, "Type '" + typename + "' has no struct export");
+				}
+			}
 		}
 		catch (TypeCheckException e)
 		{