X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2FastTHF.ml;h=e47c69e650bf52ac61a495bacb57863ebf5c2344;hb=bc389dd4724959688aafc1ede450794f47b8d0b5;hp=541cf98e14ce4ac358585ed3ee3e47e72e690de9;hpb=fedecee9c4b10a2469c10fe09ec091d2dc6fc56a;p=helm.git

diff --git a/helm/software/components/tptp_grafite/astTHF.ml b/helm/software/components/tptp_grafite/astTHF.ml
index 541cf98e1..e47c69e65 100644
--- a/helm/software/components/tptp_grafite/astTHF.ml
+++ b/helm/software/components/tptp_grafite/astTHF.ml
@@ -17,6 +17,8 @@ type role =
 
 
 type ast = 
-  | Formula of string * role * CicNotationPt.term
+  | ThfFormula of string * role * CicNotationPt.term
+  | ThfDefinition of string * string * CicNotationPt.term
+  | ThfType of string * string * CicNotationPt.term
   | Comment of string
   | Inclusion of string * (string list)