X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=614848706f5110a6398937d9548a5d305038c8cc;hb=caf8d6cf32c9a9ec8d3fba0aa912d080ff5f7d52;hp=2c46c3c46a23238d818740a18c2aec39642a7d96;hpb=b993b6f15936219a54b2c057fc75ec1b8dde243a;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 2c46c3c46..614848706 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -754,7 +754,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                 K.conclude_method = method_name;
                 K.conclude_args =
                   K.Aux (string_of_int no_constructors) 
-                  ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
+                  ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))
                   ::method_args@other_method_args;
                 K.conclude_conclusion = 
                    try Some