src/Pure/thm.ML
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, ...}, ...}, _)) =