X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fsequent2pres.ml;h=d9c3a325e808a7d531dddd37d2a9be124ff1a967;hb=b02253b371aadbbb37226a685b9bd8777a64d175;hp=2ae090bb01e1d2f0a0040c21fa7d162bdacde7c4;hpb=849b36b9489da3dc3b7b4ef1a97c574f41968876;p=helm.git

diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml
index 2ae090bb0..d9c3a325e 100644
--- a/helm/software/components/content_pres/sequent2pres.ml
+++ b/helm/software/components/content_pres/sequent2pres.ml
@@ -99,7 +99,7 @@ let sequent2pres ~ids_to_inner_sorts =
   sequent2pres
     (fun annterm ->
       let ast, ids_to_uris =
-        TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
+       TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
       in
       CicNotationPres.box_of_mpres
         (CicNotationPres.render ids_to_uris