X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fsequent2pres.ml;h=d9c3a325e808a7d531dddd37d2a9be124ff1a967;hb=488f49d2ac60fa63e65a19ad8684414266e05ac6;hp=2ae090bb01e1d2f0a0040c21fa7d162bdacde7c4;hpb=e6d7bb2e5237c8f9c85179715edeab61263ab62d;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