X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=af67f1c1454a8a367ef033b3034e1275b4be7aa0;hb=b1fb6b8e1767d775bc452303629e95941d142bea;hp=b85be0754e7194cd9efc140d365d4295339915c6;hpb=faf328f5779a7281c9c0588680b1b7bb89ae7640;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index b85be0754..af67f1c14 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -123,7 +123,9 @@ expr2:
         Hashtbl.find uri_of_id_map $1
        with
         Not_found ->
-         raise (UnknownIdentifier $1)
+	 match ! CicTextualParser0.locate_object $1 with
+	  | None      -> raise (UnknownIdentifier $1)
+	  | Some term -> Hashtbl.add uri_of_id_map $1 term; term  
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
     { let cookingno = get_cookingno (fst $5) in