X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Fparser.mly;h=4fe172144a4a2636f11f0d840c42ed07fc9f0624;hb=1652681b5eb49332f1c78e6c26d3ae5c7253d382;hp=05577000cf650f214a101af4f2a8a1d23b1e0d1e;hpb=bc76b4d2f3c380894259b45fad52cf85ae6cee18;p=helm.git

diff --git a/helm/software/components/tptp_grafite/parser.mly b/helm/software/components/tptp_grafite/parser.mly
index 05577000c..4fe172144 100644
--- a/helm/software/components/tptp_grafite/parser.mly
+++ b/helm/software/components/tptp_grafite/parser.mly
@@ -119,6 +119,11 @@
   atomic_word:
     | LNAME { $1 }
     | QSTRING { rm_q $1 }
+    | TYPE { (* workaround! *)
+      match $1 with 
+      | "theorem" -> "theoremP" 
+      | "axiom" -> "axiomP" 
+      | s -> prerr_endline s;assert false }
   ;
   
   formula_source_and_infos: