Add function t_label_remove.

src/core/term.ml

@@ -485,6 +485,9 @@ let t_label ?loc l t =
 let t_label_add l t =
   Hsterm.hashcons { t with t_label = Slab.add l t.t_label }
 
+let t_label_remove l t =
+  Hsterm.hashcons { t with t_label = Slab.remove l t.t_label }
+
 let t_label_copy { t_label = lab; t_loc = loc } t =
   let lab = Slab.union lab t.t_label in
   let loc = if t.t_loc = None then loc else t.t_loc in

src/core/term.mli

@@ -238,6 +238,7 @@ val t_exists_close : vsymbol list -> trigger -> term -> term
 
 val t_label : ?loc:Loc.position -> Slab.t -> term -> term
 val t_label_add : label -> term -> term
+val t_label_remove : label -> term -> term
 val t_label_copy : term -> term -> term
 
 (** Constructors with propositional simplification *)