src/Pure/thm.ML

--- a/src/Pure/thm.ML	Wed Jun 02 21:12:28 2010 +0200
+++ b/src/Pure/thm.ML	Wed Jun 02 21:39:35 2010 +0200
@@ -584,8 +584,8 @@
 
 (* closed derivations with official name *)
 
-fun derivation_name thm =
-  Pt.guess_name (Pt.proof_of (raw_body thm));   (* FIXME tmp *)
+fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
+  Pt.get_name shyps hyps prop (Pt.proof_of body);
 
 fun name_derivation name (thm as Thm (der, args)) =
   let