equal
deleted
inserted
replaced
255 val lookup_thm_id = Global_Theory.lookup_thm_id thy; |
255 val lookup_thm_id = Global_Theory.lookup_thm_id thy; |
256 |
256 |
257 fun proof_boxes thm thm_id = |
257 fun proof_boxes thm thm_id = |
258 let |
258 let |
259 val selection = |
259 val selection = |
260 {included = fn thm_id' => #serial thm_id = #serial thm_id', |
260 {included = Proofterm.this_id (SOME thm_id), |
261 excluded = is_some o lookup_thm_id}; |
261 excluded = is_some o lookup_thm_id}; |
262 val boxes = |
262 val boxes = |
263 map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm]) |
263 map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm]) |
264 handle Proofterm.MIN_PROOF () => Thm_Deps.thm_boxes selection [thm] |
264 handle Proofterm.MIN_PROOF () => Thm_Deps.thm_boxes selection [thm] |
265 in boxes @ [thm_id] end; |
265 in boxes @ [thm_id] end; |