X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=f69de41f553929765cc3e0cd393211939e38b2e2;hb=b68e52f889215ce2c21c3d771f59b2d2057d53c1;hp=f86d4d36e77bd0bf67b0319a795e7bc0f5a0b52f;hpb=2ecac72aa0961834dd63f0245d2ec563ea96bef2;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index f86d4d36e..f69de41f5 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -128,6 +128,7 @@ module Superposition (B : Orderings.Blob) =
     let prof_demod_u = HExtlib.profile ~enable "demod.unify";;
     let prof_demod_r = HExtlib.profile ~enable "demod.retrieve_generalizations";;
     let prof_demod_o = HExtlib.profile ~enable "demod.compare_terms";;
+    let prof_demod_s = HExtlib.profile ~enable "demod.apply_subst";;
 
     let demod table varlist subterm =
       let cands = 
@@ -145,8 +146,14 @@ module Superposition (B : Orderings.Blob) =
                    prof_demod_u.HExtlib.profile 
                      (Unif.unification (varlist@vl) varlist subterm) side 
                  in 
-                 let side = Subst.apply_subst subst side in
-                 let newside = Subst.apply_subst subst newside in
+                 let side = 
+                   prof_demod_s.HExtlib.profile 
+                     (Subst.apply_subst subst) side 
+                 in
+                 let newside = 
+                   prof_demod_s.HExtlib.profile 
+                     (Subst.apply_subst subst) newside 
+                 in
                  if o = Terms.Incomparable then
                    let o = 
                      prof_demod_o.HExtlib.profile