From 3727615c65c0d140ab5feeb41113315ecc9dbe36 Mon Sep 17 00:00:00 2001
From: denes <??>
Date: Mon, 20 Jul 2009 11:22:28 +0000
Subject: [PATCH] No demod call on functionnal symbols

---
 helm/software/components/ng_paramodulation/superposition.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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
     ;;
-- 
2.39.2