X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftptp_grafite%2Fparser.mly;h=4fe172144a4a2636f11f0d840c42ed07fc9f0624;hb=9333fdbe385f6e80b272b194e88001f28dbc8d73;hp=05577000cf650f214a101af4f2a8a1d23b1e0d1e;hpb=894b08ca7d14aa7e31c35f3acb3903a1c3472a27;p=helm.git

diff --git a/components/tptp_grafite/parser.mly b/components/tptp_grafite/parser.mly
index 05577000c..4fe172144 100644
--- a/components/tptp_grafite/parser.mly
+++ b/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: