more profilers

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index f86d4d36e77bd0bf67b0319a795e7bc0f5a0b52f..f69de41f553929765cc3e0cd393211939e38b2e2 100644 (file)
--- 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