src/HOL/Tools/TFL/casesplit.ML
changeset 29270 0eade173f77e
parent 29265 5b4247055bd7
child 31723 f5cafe803b55
equal deleted inserted replaced
29269:5c25a2012975 29270:0eade173f77e
   121       val abs_ct = ctermify abst;
   121       val abs_ct = ctermify abst;
   122       val free_ct = ctermify x;
   122       val free_ct = ctermify x;
   123 
   123 
   124       val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
   124       val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
   125 
   125 
   126       val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
   126       val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm);
   127       val (Pv, Dv, type_insts) =
   127       val (Pv, Dv, type_insts) =
   128           case (Thm.concl_of case_thm) of
   128           case (Thm.concl_of case_thm) of
   129             (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
   129             (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
   130             (Pv, Dv,
   130             (Pv, Dv,
   131              Sign.typ_match sgn (Dty, ty) Vartab.empty)
   131              Sign.typ_match sgn (Dty, ty) Vartab.empty)