X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fsequent2pres.ml;h=b1bc387581da31add8b68ac7879f3bebb605ce52;hb=585469505faa97c21687128490828a1aabee94ee;hp=b98f95634a3619e0e0e8027ae3fa278155c396f8;hpb=21d58ec6efaf1969c42eb3929475b638cdd0ce2e;p=helm.git

diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml
index b98f95634..b1bc38758 100644
--- a/helm/software/components/content_pres/sequent2pres.ml
+++ b/helm/software/components/content_pres/sequent2pres.ml
@@ -107,8 +107,7 @@ let sequent2pres ~ids_to_inner_sorts =
 
 let nsequent2pres ~subst =
   sequent2pres0
-    (fun term ->
-      let ast = NTermCicContent.nast_of_cic ~subst term in
-       CicNotationPres.box_of_mpres
-        (CicNotationPres.render (Hashtbl.create 1)
-          (TermContentPres.pp_ast ast)))
+    (fun ast ->
+      CicNotationPres.box_of_mpres
+       (CicNotationPres.render (Hashtbl.create 1)
+         (TermContentPres.pp_ast ast)))