equal
deleted
inserted
replaced
84 if member (op =) concl_vars v then (T, []) |
84 if member (op =) concl_vars v then (T, []) |
85 else (Ts ---> T, ts); |
85 else (Ts ---> T, ts); |
86 val u = Free (y, U); |
86 val u = Free (y, U); |
87 in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end; |
87 in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end; |
88 val (inst1, inst2) = |
88 val (inst1, inst2) = |
89 split_list (map (apply2 (apply2 (Proof_Context.cterm_of ctxt))) (map2 var_inst vars ys)); |
89 split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys)); |
90 |
90 |
91 val th'' = Thm.instantiate ([], inst1) th'; |
91 val th'' = Thm.instantiate ([], inst1) th'; |
92 in ((inst2, th''), ctxt'') end; |
92 in ((inst2, th''), ctxt'') end; |
93 |
93 |
94 (* |
94 (* |