407 val _ = trace_msg (fn () => |
407 val _ = trace_msg (fn () => |
408 cat_lines ("subst_translations:" :: |
408 cat_lines ("subst_translations:" :: |
409 (substs' |> map (fn (x, y) => |
409 (substs' |> map (fn (x, y) => |
410 Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ |
410 Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ |
411 Syntax.string_of_term ctxt (term_of y))))); |
411 Syntax.string_of_term ctxt (term_of y))))); |
412 in cterm_instantiate substs' i_th |
412 in cterm_instantiate substs' i_th end |
413 handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg) |
413 handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg) |
414 end; |
414 | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^ |
|
415 "\n(Perhaps you want to try \"metisFT\".)") |
415 |
416 |
416 (* INFERENCE RULE: RESOLVE *) |
417 (* INFERENCE RULE: RESOLVE *) |
417 |
418 |
418 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index |
419 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index |
419 of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars |
420 of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars |