refactor: change signature of CC.Theory.on_new_term

src/cc/Congruence_closure.ml

@@ -305,7 +305,7 @@ module Make(A: ARG) = struct
     val key_id : int
     val key : (term,lit,data) Key.t
     val on_merge : cc -> N.t -> data -> N.t -> data -> Expl.t -> unit
-    val on_new_term: cc -> term -> data option
+    val on_new_term: cc -> N.t -> term -> data option
   end
 
   type t = {
@@ -600,7 +600,7 @@ module Make(A: ARG) = struct
     let th_map =
       IM.fold
         (fun _ (module Th: THEORY with type cc=cc) th_map ->
-           match Th.on_new_term cc t with
+           match Th.on_new_term cc n t with
            | None -> th_map
            | Some v -> K_map.add Th.key v th_map)
         cc.theories K_map.empty

src/cc/Congruence_closure_intf.ml

@@ -144,7 +144,7 @@ module type S = sig
     val make :
       key:'a key ->
       on_merge:(cc -> N.t -> 'a -> N.t -> 'a -> Expl.t -> unit) ->
-      on_new_term:(cc -> term -> 'a option) ->
+      on_new_term:(cc -> N.t -> term -> 'a option) ->
       unit ->
       t
     (** Build a micro theory. It can use the callbacks above. *)

src/th-distinct/Sidekick_th_distinct.ml

@@ -95,7 +95,7 @@ module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t
         ()
       with E_exit -> ()
 
-    let on_new_term _ _ = None
+    let on_new_term _ _ _ = None
 
     let th =
       CC.Theory.make ~key ~on_merge ~on_new_term ()