src/HOL/Tools/Datatype/datatype_case.ML
changeset 32035 8e77b6a250d5
parent 31775 2b04504fcb69
child 32671 fbd224850767
     1.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -293,7 +293,7 @@
     1.4    end;
     1.5  
     1.6  fun make_case tab ctxt = gen_make_case
     1.7 -  (match_type (ProofContext.theory_of ctxt)) Envir.subst_TVars fastype_of tab ctxt;
     1.8 +  (match_type (ProofContext.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt;
     1.9  val make_case_untyped = gen_make_case (K (K Vartab.empty))
    1.10    (K (Term.map_types (K dummyT))) (K dummyT);
    1.11