equal
deleted
inserted
replaced
705 abs_inverse = Morphism.thm phi abs_inverse, |
705 abs_inverse = Morphism.thm phi abs_inverse, |
706 type_definition = Morphism.thm phi type_definition}; |
706 type_definition = Morphism.thm phi type_definition}; |
707 |
707 |
708 fun mk_absT thy repT absT repU = |
708 fun mk_absT thy repT absT repU = |
709 let |
709 let |
710 val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) []; |
710 val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) []; |
711 in Term.typ_subst_TVars rho absT end |
711 in Term.typ_subst_TVars rho absT end |
712 handle Type.TYPE_MATCH => raise Term.TYPE ("mk_absT", [repT, absT, repU], []); |
712 handle Type.TYPE_MATCH => raise Term.TYPE ("mk_absT", [repT, absT, repU], []); |
713 |
713 |
714 fun mk_repT absT repT absU = |
714 fun mk_repT absT repT absU = |
715 if absT = repT then absU |
715 if absT = repT then absU |