equal
deleted
inserted
replaced
127 (* @chunk subproof2 *) |
127 (* @chunk subproof2 *) |
128 fun subproof1 rules preds i = |
128 fun subproof1 rules preds i = |
129 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
129 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
130 let |
130 let |
131 val (prems1, prems2) = chop (length prems - length rules) prems; |
131 val (prems1, prems2) = chop (length prems - length rules) prems; |
132 val (params1, params2) = chop (length params - length preds) params; |
132 val (params1, params2) = chop (length params - length preds) (map snd params); |
133 in |
133 in |
134 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
134 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
135 THEN |
135 THEN |
136 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
136 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
137 end) |
137 end) |