equal
deleted
inserted
replaced
159 fun instT' ct = instT (Thm.ctyp_of_term ct) |
159 fun instT' ct = instT (Thm.ctyp_of_term ct) |
160 |
160 |
161 |
161 |
162 (* certified terms *) |
162 (* certified terms *) |
163 |
163 |
164 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt) |
164 fun certify ctxt = Proof_Context.cterm_of ctxt |
165 |
165 |
166 fun typ_of ct = #T (Thm.rep_cterm ct) |
166 fun typ_of ct = #T (Thm.rep_cterm ct) |
167 |
167 |
168 fun dest_cabs ct ctxt = |
168 fun dest_cabs ct ctxt = |
169 (case Thm.term_of ct of |
169 (case Thm.term_of ct of |