src/HOL/Tools/TFL/casesplit.ML
changeset 32035 8e77b6a250d5
parent 31784 bd3486c57ba3
child 32091 30e2ffbba718
equal deleted inserted replaced
32034:70c0bcd0adfb 32035:8e77b6a250d5
   127             (Pv, Dv,
   127             (Pv, Dv,
   128              Sign.typ_match sgn (Dty, ty) Vartab.empty)
   128              Sign.typ_match sgn (Dty, ty) Vartab.empty)
   129           | _ => error "not a valid case thm";
   129           | _ => error "not a valid case thm";
   130       val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
   130       val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
   131         (Vartab.dest type_insts);
   131         (Vartab.dest type_insts);
   132       val cPv = ctermify (Envir.subst_TVars type_insts Pv);
   132       val cPv = ctermify (Envir.subst_term_types type_insts Pv);
   133       val cDv = ctermify (Envir.subst_TVars type_insts Dv);
   133       val cDv = ctermify (Envir.subst_term_types type_insts Dv);
   134     in
   134     in
   135       (beta_eta_contract
   135       (beta_eta_contract
   136          (case_thm
   136          (case_thm
   137             |> Thm.instantiate (type_cinsts, [])
   137             |> Thm.instantiate (type_cinsts, [])
   138             |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])))
   138             |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])))