src/HOL/Tools/Function/pattern_split.ML
changeset 32035 8e77b6a250d5
parent 31784 bd3486c57ba3
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -39,7 +39,8 @@
     1.4           
     1.5  (* This is copied from "fundef_datatype.ML" *)
     1.6  fun inst_constrs_of thy (T as Type (name, _)) =
     1.7 -    map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
     1.8 +    map (fn (Cn,CT) =>
     1.9 +          Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    1.10          (the (Datatype.get_constrs thy name))
    1.11    | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
    1.12