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