equal
deleted
inserted
replaced
65 ---------------- |
65 ---------------- |
66 B ['b, y params] |
66 B ['b, y params] |
67 *) |
67 *) |
68 fun lift_import idx params th ctxt = |
68 fun lift_import idx params th ctxt = |
69 let |
69 let |
70 val cert = Thm.cterm_of (ProofContext.theory_of ctxt); |
70 val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); |
71 val ((_, [th']), ctxt') = Variable.importT [th] ctxt; |
71 val ((_, [th']), ctxt') = Variable.importT [th] ctxt; |
72 |
72 |
73 val Ts = map (#T o Thm.rep_cterm) params; |
73 val Ts = map (#T o Thm.rep_cterm) params; |
74 val ts = map Thm.term_of params; |
74 val ts = map Thm.term_of params; |
75 |
75 |