let rec replace_terms_in_term (term: term) (mapping: (term * term) list) : term =
let rec replace_in_term' (term: term) : term =
try
let (_, new_term) =
List.find
(fun (old_term, _) -> term_equal term old_term)
mapping
in
new_term
with
| Not_found ->
begin
match term with
| Var _
| Const _ ->
term
| Func func ->
let new_terms =
Array.map
(fun term ->
replace_in_term' term
)
func.subterms
in
request_func (func.symbol, new_terms)
end
in
replace_in_term' term