let replace_term_in_term (term: term) (old_term: term) (new_term: term) : term =
let rec replace_in_term' (term: term) : term =
if term_equal term old_term then
new_term
else
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)
in
if term_equal old_term new_term then
term
else
replace_in_term' term