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