equal
deleted
inserted
replaced
571 fun dest_env ctxt env = |
571 fun dest_env ctxt env = |
572 let |
572 let |
573 val pairs = Vartab.dest (Envir.term_env env); |
573 val pairs = Vartab.dest (Envir.term_env env); |
574 val types = Vartab.dest (Envir.type_env env); |
574 val types = Vartab.dest (Envir.type_env env); |
575 val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs; |
575 val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs; |
576 val xs = map2 (curry (Thm.cterm_of ctxt o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts); |
576 val xs = map #1 pairs ~~ map Thm.typ_of_cterm ts; |
577 in (map (fn (xi, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (xi, S), T)) types, xs ~~ ts) end; |
577 in (map (fn (ai, (S, T)) => ((ai, S), Thm.ctyp_of ctxt T)) types, xs ~~ ts) end; |
578 |
578 |
579 in |
579 in |
580 |
580 |
581 fun guess_instance ctxt rule i st = |
581 fun guess_instance ctxt rule i st = |
582 let |
582 let |