| changeset 56634 | a001337c8d24 |
| parent 56254 | a2dd9200854d |
| child 57567 | d554b0097ad4 |
--- a/src/HOL/Tools/BNF/bnf_comp.ML Wed Apr 23 09:32:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Wed Apr 23 10:23:26 2014 +0200 @@ -707,7 +707,7 @@ fun mk_absT thy repT absT repU = let - val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) []; + val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) []; in Term.typ_subst_TVars rho absT end handle Type.TYPE_MATCH => raise Term.TYPE ("mk_absT", [repT, absT, repU], []);