514 hol_terms_from_metis ctxt mode old_skolems sym_tab [m_tm, fr] |
514 hol_terms_from_metis ctxt mode old_skolems sym_tab [m_tm, fr] |
515 val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) |
515 val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) |
516 fun replace_item_list lx 0 (_::ls) = lx::ls |
516 fun replace_item_list lx 0 (_::ls) = lx::ls |
517 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls |
517 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls |
518 fun path_finder_fail tm ps t = |
518 fun path_finder_fail tm ps t = |
519 raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ |
519 raise METIS ("equality_inference (path_finder)", |
520 "equality_inference, path_finder: path = " ^ |
520 "path = " ^ space_implode " " (map string_of_int ps) ^ |
521 space_implode " " (map string_of_int ps) ^ |
521 " isa-term: " ^ Syntax.string_of_term ctxt tm ^ |
522 " isa-term: " ^ Syntax.string_of_term ctxt tm ^ |
522 (case t of |
523 (case t of |
523 SOME t => " fol-term: " ^ Metis_Term.toString t |
524 SOME t => " fol-term: " ^ Metis_Term.toString t |
524 | NONE => "")) |
525 | NONE => "")) |
|
526 fun path_finder_FO tm [] = (tm, Bound 0) |
525 fun path_finder_FO tm [] = (tm, Bound 0) |
527 | path_finder_FO tm (p::ps) = |
526 | path_finder_FO tm (p::ps) = |
528 let val (tm1,args) = strip_comb tm |
527 let val (tm1,args) = strip_comb tm |
529 val adjustment = get_ty_arg_size thy tm1 |
528 val adjustment = get_ty_arg_size thy tm1 |
530 val p' = if adjustment > p then p else p - adjustment |
529 val p' = if adjustment > p then p else p - adjustment |