equal
deleted
inserted
replaced
253 val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; |
253 val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; |
254 |
254 |
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_of thm thm_id = |
257 fun proof_boxes_of thm thm_id = |
258 if export_standard_proofs then [] |
258 let |
259 else |
259 val dep_boxes = |
260 let |
260 thm |> Thm_Deps.proof_boxes (fn thm_id' => |
261 val dep_boxes = |
261 if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id')); |
262 thm |> Thm_Deps.proof_boxes (fn thm_id' => |
262 in dep_boxes @ [thm_id] end; |
263 if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id')); |
|
264 in dep_boxes @ [thm_id] end; |
|
265 |
263 |
266 fun expand_name thm_id (header: Proofterm.thm_header) = |
264 fun expand_name thm_id (header: Proofterm.thm_header) = |
267 if #serial header = #serial thm_id then "" |
265 if #serial header = #serial thm_id then "" |
268 else |
266 else |
269 (case lookup_thm_id (Proofterm.thm_header_id header) of |
267 (case lookup_thm_id (Proofterm.thm_header_id header) of |