changeset 70603 | 706dac15554b |
parent 70595 | 2ae7e33c950f |
child 70812 | 3ae7949ef059 |
--- a/src/Pure/thm.ML Wed Aug 21 20:08:50 2019 +0200 +++ b/src/Pure/thm.ML Fri Aug 23 13:20:13 2019 +0200 @@ -993,8 +993,7 @@ (*identified PThm node*) fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) = - Proofterm.get_id shyps hyps prop (proof_of thm) - handle Proofterm.MIN_PROOF => NONE; + Proofterm.get_id shyps hyps prop (proof_of thm); (*dependencies of PThm node*) fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) =