No demod call on functionnal symbols

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 0a7c5cfcc1c82fdb0be718e4ddde26bca391d876..dd394ce675450f1a6b3083c875d3c7dd20907664 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -81,7 +81,7 @@ module Superposition (B : Orderings.Blob) =
       let rec aux bag pos ctx id = function
       | Terms.Leaf _ as t -> f bag t pos ctx id
       | Terms.Var _ as t -> bag,t,id
-      | Terms.Node l as t->
+      | Terms.Node (hd::l) as t->
           let bag,t,id1 = f bag t pos ctx id in
             if id = id1 then
               let bag, l, _, id = 
@@ -92,10 +92,11 @@ module Superposition (B : Orderings.Blob) =
                      let bag,newt,id = aux bag newpos newctx id t in
                        if post = [] then bag, pre@[newt], [], id
                        else bag, pre @ [newt], List.tl post, id)
-                  (bag, [], List.tl l, id) l
+                  (bag, [hd], List.tl l, id) l
               in
                 bag, Terms.Node l, id
             else bag,t,id1
+      | _ -> assert false
       in
         aux bag pos ctx id t
     ;;