equal
deleted
inserted
replaced
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) |