let request_func ?(insert_db:bool = true) ((symbol, terms): symbol * term array) : term =
  if Const.debug then begin
    if (Symbol.arity symbol != Array.length terms) then begin
      print_newline ();
      print_endline (Symbol.to_string symbol);
      print_endline (string_of_int (Symbol.arity symbol));
      Array.iter (fun term -> print_endline (term_to_string term)) terms;
      failwith "request_func: arity mismatch";
    end;
  end;

  let new_term =
    Func (*(symbol, terms, compute_hash symbol terms)*)
      {
        symbol = symbol;
        subterms = terms;
        ground = Tools.array_for_all is_term_ground terms;
        hash = compute_hash symbol terms;
        in_db = insert_db;
      }
  in
   request_term ~insert_db:insert_db new_term