equal
deleted
inserted
replaced
186 (*Determine print names of goal parameters (reversed)*) |
186 (*Determine print names of goal parameters (reversed)*) |
187 fun innermost_params i st = |
187 fun innermost_params i st = |
188 let val (_, _, Bi, _) = dest_state (st, i) |
188 let val (_, _, Bi, _) = dest_state (st, i) |
189 in Term.rename_wrt_term Bi (Logic.strip_params Bi) end; |
189 in Term.rename_wrt_term Bi (Logic.strip_params Bi) end; |
190 |
190 |
191 (*params of subgoal i as they are printed*) |
|
192 fun params_of_state i st = rev (innermost_params i st); |
|
193 |
|
194 |
191 |
195 (*** Applications of cut_rl ***) |
192 (*** Applications of cut_rl ***) |
196 |
193 |
197 (*The conclusion of the rule gets assumed in subgoal i, |
194 (*The conclusion of the rule gets assumed in subgoal i, |
198 while subgoal i+1,... are the premises of the rule.*) |
195 while subgoal i+1,... are the premises of the rule.*) |