src/Pure/thm.ML

   val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
   val name_derivation: string -> thm -> thm
+  val close_derivation: thm -> thm
   val axiom: theory -> string -> thm
   val axioms_of: theory -> (string * thm) list
   val get_tags: thm -> Properties.T
   val map_tags: (Properties.T -> Properties.T) -> thm -> thm
   val norm_proof: thm -> thm

 
     val ps = map (apsnd (Future.map fulfill_body)) promises;
     val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body;
     val der' = make_deriv [] [] [pthm] proof;
   in Thm (der', args) end;
+
+fun close_derivation thm =
+  if derivation_closed thm then thm else name_derivation "" thm;
 
 
 
 (** Axioms **)