X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2FastTHF.ml;h=e47c69e650bf52ac61a495bacb57863ebf5c2344;hb=f3c3059ab94266de1cdf7cbd1bbc62231d2f9a22;hp=541cf98e14ce4ac358585ed3ee3e47e72e690de9;hpb=dd29593d12cffd332c9d546167215f42a90fa9f7;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)