equal
deleted
inserted
replaced
464 fun path_finder_FO tm [] = (tm, Bound 0) |
464 fun path_finder_FO tm [] = (tm, Bound 0) |
465 | path_finder_FO tm (p::ps) = |
465 | path_finder_FO tm (p::ps) = |
466 let val (tm1,args) = strip_comb tm |
466 let val (tm1,args) = strip_comb tm |
467 val adjustment = get_ty_arg_size thy tm1 |
467 val adjustment = get_ty_arg_size thy tm1 |
468 val p' = if adjustment > p then p else p-adjustment |
468 val p' = if adjustment > p then p else p-adjustment |
469 val tm_p = List.nth(args,p') |
469 val tm_p = nth args p' |
470 handle Subscript => |
470 handle Subscript => |
471 error ("Cannot replay Metis proof in Isabelle:\n" ^ |
471 error ("Cannot replay Metis proof in Isabelle:\n" ^ |
472 "equality_inf: " ^ string_of_int p ^ " adj " ^ |
472 "equality_inf: " ^ string_of_int p ^ " adj " ^ |
473 string_of_int adjustment ^ " term " ^ |
473 string_of_int adjustment ^ " term " ^ |
474 Syntax.string_of_term ctxt tm) |
474 Syntax.string_of_term ctxt tm) |