From: denes <??>
Date: Mon, 20 Jul 2009 11:22:28 +0000 (+0000)
Subject: No demod call on functionnal symbols
X-Git-Tag: make_still_working~3656
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3727615c65c0d140ab5feeb41113315ecc9dbe36;p=helm.git

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 0a7c5cfcc..dd394ce67 100644
--- 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
     ;;