src/HOL/Tools/TFL/casesplit.ML
changeset 32035 8e77b6a250d5
parent 31784 bd3486c57ba3
child 32091 30e2ffbba718
     1.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -129,8 +129,8 @@
     1.4            | _ => error "not a valid case thm";
     1.5        val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
     1.6          (Vartab.dest type_insts);
     1.7 -      val cPv = ctermify (Envir.subst_TVars type_insts Pv);
     1.8 -      val cDv = ctermify (Envir.subst_TVars type_insts Dv);
     1.9 +      val cPv = ctermify (Envir.subst_term_types type_insts Pv);
    1.10 +      val cDv = ctermify (Envir.subst_term_types type_insts Dv);
    1.11      in
    1.12        (beta_eta_contract
    1.13           (case_thm