From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 13:39:19 +0000 (+0000)
Subject: Bug fixed: singleton application.
X-Git-Tag: make_still_working~3670
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=65792c85896dab2d3c69e7eafd8ff5c628260773;p=helm.git

Bug fixed: singleton application.
---

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 350144f9e..0c1a98ec3 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -107,7 +107,7 @@ let mk_elim uri leftno [it] (outsort,suffix) =
      let cargs,recursive_args = List.split cargs_and_recursive_args in
      let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in
       CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs),
-       CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args)
+       mk_appl (name_of_k name :: cargs @ recursive_args)
    ) cl
  in
  let bo = CicNotationPt.Case (rec_arg,None,None,branches) in