src/Pure/thm.ML

   val future: thm future -> cterm -> thm
   val thm_deps: thm -> Proofterm.thm Ord_List.T
   val extra_shyps: thm -> sort list
   val strip_shyps: thm -> thm
   val derivation_closed: thm -> bool
-  val derivation_name: thm -> string
+  val derivation_name: thm -> Thm_Name.T
   val derivation_id: thm -> Proofterm.thm_id option
-  val raw_derivation_name: thm -> string
-  val expand_name: thm -> Proofterm.thm_header -> string option
-  val name_derivation: string * Position.T -> thm -> thm
+  val raw_derivation_name: thm -> Thm_Name.T
+  val expand_name: thm -> Proofterm.thm_header -> Thm_Name.T option
+  val name_derivation: Thm_Name.P -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
   val axiom: theory -> string -> thm
   val all_axioms_of: theory -> (string * thm) list
   val get_tags: thm -> Properties.T

   let
     val self_id =
       (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of
         NONE => K false
       | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header);
-    fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE;
+    fun expand header =
+      if self_id header orelse Thm_Name.is_empty (#thm_name header)
+      then SOME Thm_Name.empty else NONE;
   in expand end;
 
 (*deterministic name of finished proof*)
 fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
   Proofterm.get_approximative_name shyps hyps prop (proof_of thm);

     in Thm (make_deriv0 [] body', args) end);
 
 fun close_derivation pos =
   solve_constraints #> (fn thm =>
     if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
-    else name_derivation ("", pos) thm);
+    else name_derivation (Thm_Name.empty, pos) thm);
 
 val trim_context = solve_constraints #> trim_context_thm;