X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=bf80a5939b47153dd938a84f4a4e2ca96ef65127;hb=d6bdacb3cf305051e9e19f8b0422a33315a9279b;hp=2cc72933b884cbaca2eeea3ddc2b1d51ed625db3;hpb=caf8d6cf32c9a9ec8d3fba0aa912d080ff5f7d52;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 2cc72933b..bf80a5939 100644
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -210,15 +210,9 @@ let proof2cic deannotate p =
                with Not_found -> 
                   prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
                   raise Not_found))
-      | Con.Lemma lemma -> 
-          MQueryMisc.term_of_cic_textual_parser_uri 
-           (MQueryMisc.cic_textual_parser_uri_of_string
-            (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
-              lemma.Con.lemma_uri))
-      | Con.Term t -> 
-          deannotate t
-      | Con.ArgProof p ->
-          proof2cic [] p (* empty! *)
+      | Con.Lemma lemma -> CicUtil.term_of_uri lemma.Con.lemma_uri
+      | Con.Term t -> deannotate t
+      | Con.ArgProof p -> proof2cic [] p (* empty! *)
       | Con.ArgMethod s -> raise TO_DO
 
 in proof2cic [] p