| changeset 41699 | 21492e1c2b5a |
| parent 40238 | edcdecd55655 |
| child 41700 | f33d5a00c25d |
--- a/src/Pure/thm.ML Thu Feb 03 19:21:12 2011 +0100 +++ b/src/Pure/thm.ML Thu Feb 03 19:27:04 2011 +0100 @@ -576,6 +576,7 @@ (* closed derivations with official name *) +(*non-deterministic, depends on unknown promises*) fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);