equal
deleted
inserted
replaced
54 val case_thm = case_thm_of_ty sgn ty; |
54 val case_thm = case_thm_of_ty sgn ty; |
55 |
55 |
56 val abs_ct = ctermify abst; |
56 val abs_ct = ctermify abst; |
57 val free_ct = ctermify x; |
57 val free_ct = ctermify x; |
58 |
58 |
59 val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm)); |
59 val casethm_vars = rev (Misc_Legacy.term_vars (Thm.concl_of case_thm)); |
60 |
60 |
61 val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm); |
61 val casethm_tvars = Misc_Legacy.term_tvars (Thm.concl_of case_thm); |
62 val (Pv, Dv, type_insts) = |
62 val (Pv, Dv, type_insts) = |
63 case (Thm.concl_of case_thm) of |
63 case (Thm.concl_of case_thm) of |
64 (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => |
64 (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => |
65 (Pv, Dv, |
65 (Pv, Dv, |
66 Sign.typ_match sgn (Dty, ty) Vartab.empty) |
66 Sign.typ_match sgn (Dty, ty) Vartab.empty) |