equal
deleted
inserted
replaced
374 val (tm1, args) = strip_comb tm |
374 val (tm1, args) = strip_comb tm |
375 val adjustment = length ts - length args |
375 val adjustment = length ts - length args |
376 val p' = if adjustment > p then p else p - adjustment |
376 val p' = if adjustment > p then p else p - adjustment |
377 val tm_p = |
377 val tm_p = |
378 nth args p' |
378 nth args p' |
379 handle Subscript => path_finder_fail tm (p :: ps) (SOME t) |
379 handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t) |
380 val _ = trace_msg ctxt (fn () => |
380 val _ = trace_msg ctxt (fn () => |
381 "path_finder: " ^ string_of_int p ^ " " ^ |
381 "path_finder: " ^ string_of_int p ^ " " ^ |
382 Syntax.string_of_term ctxt tm_p) |
382 Syntax.string_of_term ctxt tm_p) |
383 val (r, t) = path_finder tm_p ps (nth ts p) |
383 val (r, t) = path_finder tm_p ps (nth ts p) |
384 in (r, list_comb (tm1, replace_item_list t p' args)) end |
384 in (r, list_comb (tm1, replace_item_list t p' args)) end |