equal
deleted
inserted
replaced
278 let |
278 let |
279 val cert = Thm.cterm_of thy; |
279 val cert = Thm.cterm_of thy; |
280 fun prep_var (x, SOME t) = |
280 fun prep_var (x, SOME t) = |
281 let |
281 let |
282 val cx = cert x; |
282 val cx = cert x; |
283 val {T = xT, thy, ...} = Thm.rep_cterm cx; |
283 val xT = #T (Thm.rep_cterm cx); |
284 val ct = cert (tune t); |
284 val ct = cert (tune t); |
|
285 val tT = Thm.ctyp_of_term ct; |
285 in |
286 in |
286 if Type.could_unify (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) |
287 if Type.could_unify (Thm.typ_of tT, xT) then SOME (cx, ct) |
287 else error (Pretty.string_of (Pretty.block |
288 else error (Pretty.string_of (Pretty.block |
288 [Pretty.str "Ill-typed instantiation:", Pretty.fbrk, |
289 [Pretty.str "Ill-typed instantiation:", Pretty.fbrk, |
289 Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, |
290 Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, |
290 Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) |
291 Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) |
291 end |
292 end |
430 |
431 |
431 in |
432 in |
432 |
433 |
433 fun guess_instance rule i st = |
434 fun guess_instance rule i st = |
434 let |
435 let |
435 val {thy, maxidx, ...} = Thm.rep_thm st; |
436 val thy = Thm.theory_of_thm st; |
|
437 val maxidx = Thm.maxidx_of st; |
436 val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) |
438 val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) |
437 val params = rev (rename_wrt_term goal (Logic.strip_params goal)); |
439 val params = rev (rename_wrt_term goal (Logic.strip_params goal)); |
438 in |
440 in |
439 if not (null params) then |
441 if not (null params) then |
440 (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ |
442 (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ |