From a8d65eeb54b1accd65b0f1a9be763297d0f8b331 Mon Sep 17 00:00:00 2001
From: Nick Battle <nick.battle@gmail.com>
Date: Fri, 1 Dec 2023 10:37:10 +0000
Subject: [PATCH] And allow ! types for imports of inv_T

---
 .../java/com/fujitsu/vdmj/syntax/ModuleReader.java | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/syntax/ModuleReader.java b/vdmj/src/main/java/com/fujitsu/vdmj/syntax/ModuleReader.java
index 09fdfa222..31154ef4d 100644
--- a/vdmj/src/main/java/com/fujitsu/vdmj/syntax/ModuleReader.java
+++ b/vdmj/src/main/java/com/fujitsu/vdmj/syntax/ModuleReader.java
@@ -655,7 +655,19 @@ private ASTImportedFunction readImportedFunction(LexIdentifierToken from)
 		if (lastToken().is(Token.COLON))
 		{
 			nextToken();
-			type = getTypeReader().readType();
+			
+			// Allow maximal ! for inv_T functions
+			boolean saved = Properties.parser_maximal_types;
+			
+			try
+			{
+				Properties.parser_maximal_types = true;
+				type = getTypeReader().readType();
+			}
+			finally
+			{
+				Properties.parser_maximal_types = saved;
+			}
 		}
 
 		LexNameToken renamed = null;