diff --git a/src/Refinements-Parsing/NNFParser.class.st b/src/Refinements-Parsing/NNFParser.class.st
index a95620162..7d3f335a8 100644
--- a/src/Refinements-Parsing/NNFParser.class.st
+++ b/src/Refinements-Parsing/NNFParser.class.st
@@ -3,7 +3,6 @@ Class {
 	#superclass : #FixpointParser,
 	#instVars : [
 		'hCstr',
-		'var',
 		'sort',
 		'hBind',
 		'symSort',
@@ -97,7 +96,7 @@ NNFParser >> hQualifier [
 NNFParser >> hThing [
 	^(
 		  ('constraint' asParser trim, hCstr ==> #second)
-		/ var
+		/ self hVar
 		/ self hQualifier
 		/ ('constant' asParser trim, self tok trim, sort ==> [ :x | HCon symbol: x second sort: x third ])
 		/ self fixpoint
@@ -107,6 +106,15 @@ NNFParser >> hThing [
 	) parens
 ]
 
+{ #category : #grammar }
+NNFParser >> hVar [
+	^'var' asParser trim,
+	self kvSym trim,
+	sort parens trim plus parens
+	==> [ :x | HVar name: x second argSorts: x third ]
+	
+]
+
 { #category : #grammar }
 NNFParser >> kvSym [
 	^('$' asParser,
@@ -157,15 +165,6 @@ NNFParser >> tvar [
 	/ ($` asParser, #lowercase asParser ==> [ :x | Z3Sort uninterpretedSortNamed: (String with: x second) ])
 ]
 
-{ #category : #grammar }
-NNFParser >> var [
-	^'var' asParser trim,
-	self kvSym trim,
-	sort parens trim plus parens
-	==> [ :x | HVar name: x second argSorts: x third ]
-	
-]
-
 { #category : #grammar }
 NNFParser >> varSort [
 	^'@(' asParser, PPParser decimalInteger, ')' asParser