From 5699090a60ae483b38e7ddfcea489d8aea274be5 Mon Sep 17 00:00:00 2001
From: Martin Suda <martin.suda@cvut.cz>
Date: Mon, 23 Mar 2026 16:04:38 +0100
Subject: [PATCH] fix: pushed proxies are terms (TM)

---
 Parse/TPTP.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp
index 0cffdca14..74a5a12c5 100644
--- a/Parse/TPTP.cpp
+++ b/Parse/TPTP.cpp
@@ -1505,13 +1505,15 @@ void TPTP::holFormula()
   case T_SIGMA:
     resetToks();
     readTypeArgs(1);
-    _termLists.push(createFunctionApplication("vSIGMA", 1));    
+    _termLists.push(createFunctionApplication("vSIGMA", 1));
+    _lastPushed = TM;
     return;
   
   case T_PI:
     resetToks();
     readTypeArgs(1);
-    _termLists.push(createFunctionApplication("vPI", 1));      
+    _termLists.push(createFunctionApplication("vPI", 1));
+    _lastPushed = TM;
     return;
 
   case T_FORALL:
@@ -1540,6 +1542,7 @@ void TPTP::holFormula()
     ASS(_connectives.top() == NOT);
     _connectives.pop();
     _termLists.push(createFunctionApplication("vNOT", 0));
+    _lastPushed = TM;
     return;
   }