X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2FmainTHF.ml;h=aa68fa61eb738e7909e17e9abc5a5fd0cf2e842a;hb=ebe0d316f0bd186c4f0f3b1a9107e122d7878bc6;hp=ece02f4a0cc2d66b672f8d3fd4d7e6eba676d1b6;hpb=f3c3059ab94266de1cdf7cbd1bbc62231d2f9a22;p=helm.git

diff --git a/helm/software/components/tptp_grafite/mainTHF.ml b/helm/software/components/tptp_grafite/mainTHF.ml
index ece02f4a0..aa68fa61e 100644
--- a/helm/software/components/tptp_grafite/mainTHF.ml
+++ b/helm/software/components/tptp_grafite/mainTHF.ml
@@ -91,7 +91,7 @@ let _ =
            GA.NObj(floc,
             T.Theorem(`Definition,
              id,ty,Some body,`Regular)))):: aux tl
-      | A.ThfFormula(name,(A.Hypothesis|A.Assumption),term) :: tl -> 
+      | A.ThfFormula(name,(A.Axiom|A.Hypothesis|A.Assumption),term) :: tl -> 
          GA.Executable(floc,
           GA.NCommand(floc,
            GA.NObj(floc,