changeset 70979 | 7abe5abb4c05 |
parent 70976 | d86798eddc14 |
child 70981 | a802d42c00bc |
--- a/src/Pure/Thy/export_theory.ML Fri Nov 01 14:30:22 2019 +0100 +++ b/src/Pure/Thy/export_theory.ML Fri Nov 01 15:09:55 2019 +0100 @@ -257,7 +257,7 @@ fun proof_boxes thm thm_id = let val selection = - {included = fn thm_id' => #serial thm_id = #serial thm_id', + {included = Proofterm.this_id (SOME thm_id), excluded = is_some o lookup_thm_id}; val boxes = map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm])