equal
deleted
inserted
replaced
534 (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) |
534 (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) |
535 | path_finder_FT tm ps t = path_finder_fail FT tm ps (SOME t) |
535 | path_finder_FT tm ps t = path_finder_fail FT tm ps (SOME t) |
536 fun path_finder_MX tm [] _ = (tm, Bound 0) |
536 fun path_finder_MX tm [] _ = (tm, Bound 0) |
537 | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = |
537 | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = |
538 let val s = s |> unmangled_const_name in |
538 let val s = s |> unmangled_const_name in |
539 if s = metis_type_tag orelse s = prefixed_type_tag_name then |
539 if s = metis_predicator orelse s = prefixed_predicator_name orelse |
|
540 s = metis_type_tag orelse s = prefixed_type_tag_name then |
540 path_finder_MX tm ps (nth ts p) |
541 path_finder_MX tm ps (nth ts p) |
541 else if s = metis_app_op orelse s = prefixed_app_op_name then |
542 else if s = metis_app_op orelse s = prefixed_app_op_name then |
542 let |
543 let |
543 val (tm1, tm2) = dest_comb tm |
544 val (tm1, tm2) = dest_comb tm |
544 val p' = p - (length ts - 2) |
545 val p' = p - (length ts - 2) |