Bug fixed: singleton application.

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 350144f9e430307d5983f56a0590d9d1fa936de2..0c1a98ec342a9848406f925bc60056257afa1a59 100644 (file)
--- 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