diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index a67cc165f944a9de017190f77c7da7bf3779a25f..051f997cdb1c6f19497689f03a8281473d466e28 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -268,15 +268,6 @@ module Find_new_event = struct
     acc
 end
 
-let process_inverted_path d n acc =
-  let acc = List.sort_uniq InvertedPath.compare acc in
-  let acc =
-    List.fold_left
-      (fun acc ip -> InvertedPath.exec d acc Pattern.init n ip)
-      Trigger.M.empty acc
-  in
-  Trigger.M.iter (fun tri substs -> Trigger.instantiate_many d tri substs) acc
-
 module Delayed_find_new_event : sig
   val enqueue : _ Egraph.t -> Node.t -> InvertedPath.t list -> unit
 end = struct
@@ -447,14 +438,15 @@ let add_info_on_ground_terms d thg =
     match Egraph.get_dom d Info.dom repr with
     | None ->
         Egraph.set_dom d Info.dom repr info;
-        process_inverted_path d repr (Find_new_event.one d repr info [])
+        Delayed_find_new_event.enqueue d repr
+          (Find_new_event.one d repr info [])
     | Some info' ->
         Egraph.set_dom d Info.dom repr (Info.merge d ~repr ~other info info');
         (* The type is added (during registration) after the parents found in info' *)
         Find_new_event.one_pt d repr info' g.ty []
         |> Find_new_event.one d repr info
         |> Find_new_event.two d repr info repr info'
-        |> process_inverted_path d repr
+        |> Delayed_find_new_event.enqueue d repr
   in
   let add_pc pos n =
     merge_info n