do not infer on closed goals

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 435c95024416b3f232ce280855605de6e0cc1fb1..6c3c5118d62362eadc982fa63ecfbd9672b635cc 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -168,8 +168,7 @@ module Paramod (B : Terms.Blob) = struct
       let bag, maxvar, new_goals = 
         List.fold_left 
           (fun (bag,m,acc) g -> 
-             let bag, m, ng = Sup.infer_left bag m g
-               ([current],ctable) in
+             let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
                bag,m,ng@acc) 
           (bag,maxvar,[]) g_actives 
       in