parameter sintax added to axiom statement

[helm.git] / helm / software / components / tptp_grafite / mainTHF.ml

diff --git a/helm/software/components/tptp_grafite/mainTHF.ml b/helm/software/components/tptp_grafite/mainTHF.ml
index ece02f4a0cc2d66b672f8d3fd4d7e6eba676d1b6..aa68fa61eb738e7909e17e9abc5a5fd0cf2e842a 100644 (file)
--- 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,