let app_fun name args = try let vars, f = Hstring.H.find function_defs name in (* eprintf "app fun %a (%a)@." Hstring.print name Variable.print_vars vars; *) let nvars, nargs = List.length vars, List.length args in if nvars <> nargs then failwith (asprintf "Wrong arity: %a takes %d arguments but was given %d." Hstring.print name nvars nargs); let sigma = List.combine vars args in (* eprintf "app fun subst : %a@." print_subst sigma; *) (* eprintf "app fun in : %a@." print f; *) let r = apply_subst sigma f in (* eprintf "result : %a@." print r; *) r with Not_found -> failwith (asprintf "Undefined function symbol %a." Hstring.print name)