clarified expand_proof/expand_name: allow more detailed control via thm_header;
export_standard_proofs: authentic theorem names in "print" format;

--- a/src/Doc/Implementation/Logic.thy	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sun Oct 20 20:38:22 2019 +0200
@@ -1189,7 +1189,7 @@
   @{index_ML Proofterm.reconstruct_proof:
   "theory -> term -> proof -> proof"} \\
   @{index_ML Proofterm.expand_proof: "theory ->
-  (string * term option) list -> proof -> proof"} \\
+  (Proofterm.thm_header -> string option) -> proof -> proof"} \\
   @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
   @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
   @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
@@ -1228,10 +1228,11 @@
   for proofs that are constructed manually, but not for those produced
   automatically by the inference kernel.
 
-  \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<open>thy [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
-  reconstructs the proofs of all specified theorems, with the given (full)
-  proof. Theorems that are not unique specified via their name may be
-  disambiguated by giving their proposition.
+  \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<open>thy expand prf\<close> reconstructs and expands
+  the proofs of nested theorems according to the given \<open>expand\<close> function: a
+  result of @{ML \<open>SOME ""\<close>} means full expansion, @{ML \<open>SOME\<close>}~\<open>name\<close> means to
+  keep the theorem node but replace its internal name, @{ML NONE} means no
+  change.
 
   \<^descr> \<^ML>\<open>Proof_Checker.thm_of_proof\<close>~\<open>thy prf\<close> turns the given (full) proof
   into a theorem, by replaying it using only primitive rules of the inference

--- a/src/HOL/Proofs/ex/XML_Data.thy	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Sun Oct 20 20:38:22 2019 +0200
@@ -15,7 +15,7 @@
   fun export_proof thy thm =
     Proofterm.encode (Sign.consts_of thy)
       (Proofterm.reconstruct_proof thy (Thm.prop_of thm)
-        (Thm.standard_proof_of {full = true, expand = [Thm.raw_derivation_name thm]} thm));
+        (Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} thm));
 
   fun import_proof thy xml =
     let

--- a/src/HOL/Tools/inductive_realizer.ML	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Oct 20 20:38:22 2019 +0200
@@ -19,11 +19,10 @@
     [name] => name
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
-fun prf_of thy raw_thm =
-  let val thm = Thm.transfer thy raw_thm in
-    Thm.reconstruct_proof_of thm
-    |> Proofterm.expand_proof (Thm.theory_of_thm thm) [("", NONE)]
-  end;
+fun prf_of thy =
+  Thm.transfer thy #>
+  Thm.reconstruct_proof_of #>
+  Proofterm.expand_proof thy Proofterm.expand_name_empty;
 
 fun subsets [] = [[]]
   | subsets (x::xs) =

--- a/src/Pure/Proof/extraction.ML	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Sun Oct 20 20:38:22 2019 +0200
@@ -504,9 +504,11 @@
     val procs = maps (rev o fst o snd) types;
     val rtypes = map fst types;
     val typroc = typeof_proc [];
+    fun expand_name ({name, ...}: Proofterm.thm_header) =
+      if name = "" orelse member (op =) expand name then SOME "" else NONE;
     val prep = the_default (K I) prep thy' o
       Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
-      Proofterm.expand_proof thy' (map (rpair NONE) ("" :: expand));
+      Proofterm.expand_proof thy' expand_name;
     val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
 
     fun find_inst prop Ts ts vs =

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sun Oct 20 20:38:22 2019 +0200
@@ -261,14 +261,14 @@
       if r then
         let
           val cnames = map (fst o dest_Const o fst) defs';
-          val thms = Proofterm.fold_proof_atoms true
-            (fn PThm ({name, prop, ...}, _) =>
+          val expand = Proofterm.fold_proof_atoms true
+            (fn PThm ({serial, name, prop, ...}, _) =>
                 if member (op =) defnames name orelse
                   not (exists_Const (member (op =) cnames o #1) prop)
                 then I
-                else cons (name, SOME prop)
-              | _ => I) [prf] [];
-        in Proofterm.expand_proof thy thms prf end
+                else Inttab.update (serial, "")
+              | _ => I) [prf] Inttab.empty;
+        in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end
       else prf;
   in
     rewrite_terms (Pattern.rewrite_term thy defs' [])
@@ -360,7 +360,7 @@
 
     fun reconstruct prop =
       Proofterm.reconstruct_proof thy prop #>
-      Proofterm.expand_proof thy [("", NONE)] #>
+      Proofterm.expand_proof thy Proofterm.expand_name_empty #>
       Same.commit (Proofterm.map_proof_same Same.same Same.same of_class_index);
   in
     map2 reconstruct (Logic.mk_of_sort (T, S))

--- a/src/Pure/Proof/proof_syntax.ML	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Oct 20 20:38:22 2019 +0200
@@ -196,7 +196,6 @@
     (Proofterm.term_of_proof prf);
 
 fun pretty_standard_proof_of ctxt full thm =
-  pretty_proof ctxt
-    (Thm.standard_proof_of {full = full, expand = [Thm.raw_derivation_name thm]} thm);
+  pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
 
 end;

--- a/src/Pure/Thy/export_theory.ML	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun Oct 20 20:38:22 2019 +0200
@@ -263,6 +263,13 @@
               if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id'));
         in dep_boxes @ [thm_id] end;
 
+    fun expand_name thm_id (header: Proofterm.thm_header) =
+      if #serial header = #serial thm_id then ""
+      else
+        (case lookup_thm_id (Proofterm.thm_header_id header) of
+          NONE => ""
+        | SOME thm_name => Thm_Name.print thm_name);
+
     fun entity_markup_thm (serial, (name, i)) =
       let
         val space = Facts.space_of (Global_Theory.facts_of thy);
@@ -270,15 +277,15 @@
         val {pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
 
-    fun encode_thm (thm_id, thm_name) raw_thm =
+    fun encode_thm thm_id raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
         val thm = Thm.unconstrainT (clean_thm raw_thm);
         val boxes = proof_boxes_of thm thm_id;
 
         val proof0 =
-          if export_standard_proofs
-          then Thm.standard_proof_of {full = true, expand = [Thm_Name.flatten thm_name]} thm
+          if export_standard_proofs then
+            Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm
           else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
           else MinProof;
         val (prop, SOME proof) =
@@ -297,7 +304,7 @@
       let
         val markup = entity_markup_thm (#serial thm_id, thm_name);
         val thm = Global_Theory.get_thm_name thy (thm_name, Position.none);
-        val body = encode_thm (thm_id, thm_name) thm;
+        val body = encode_thm thm_id thm;
       in YXML.buffer (XML.Elem (markup, body)) end;
 
     val _ =

--- a/src/Pure/more_thm.ML	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Pure/more_thm.ML	Sun Oct 20 20:38:22 2019 +0200
@@ -114,7 +114,8 @@
   val untag: string -> attribute
   val kind: string -> attribute
   val reconstruct_proof_of: thm -> Proofterm.proof
-  val standard_proof_of: {full: bool, expand: string list} -> thm -> Proofterm.proof
+  val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
+    thm -> Proofterm.proof
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
   val show_consts: bool Config.T
@@ -656,10 +657,10 @@
 fun reconstruct_proof_of thm =
   Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
 
-fun standard_proof_of {full, expand} thm =
+fun standard_proof_of {full, expand_name} thm =
   let val thy = Thm.theory_of_thm thm in
     reconstruct_proof_of thm
-    |> Proofterm.expand_proof thy (map (rpair NONE) ("" :: expand))
+    |> Proofterm.expand_proof thy expand_name
     |> Proofterm.rew_proof thy
     |> Proofterm.no_thm_proofs
     |> not full ? Proofterm.shrink_proof

--- a/src/Pure/proofterm.ML	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Pure/proofterm.ML	Sun Oct 20 20:38:22 2019 +0200
@@ -162,7 +162,8 @@
   val reconstruct_proof: theory -> term -> proof -> proof
   val prop_of': term list -> proof -> term
   val prop_of: proof -> term
-  val expand_proof: theory -> (string * term option) list -> proof -> proof
+  val expand_name_empty: thm_header -> string option
+  val expand_proof: theory -> (thm_header -> string option) -> proof -> proof
 
   val standard_vars: Name.context -> term * proof option -> term * proof option
   val standard_vars_term: Name.context -> term -> term
@@ -178,9 +179,12 @@
   val unconstrain_thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> sort list -> term ->
     (serial * proof_body future) list -> proof_body -> thm * proof
+  val get_identity: sort list -> term list -> term -> proof ->
+    {serial: serial, theory_name: string, name: string} option
   val get_approximative_name: sort list -> term list -> term -> proof -> string
   type thm_id = {serial: serial, theory_name: string}
   val make_thm_id: serial * string -> thm_id
+  val thm_header_id: thm_header -> thm_id
   val thm_id: thm -> thm_id
   val get_id: sort list -> term list -> term -> proof -> thm_id option
 end
@@ -1935,11 +1939,10 @@
 
 (* expand and reconstruct subproofs *)
 
-fun expand_proof thy thms prf =
+fun expand_name_empty (header: thm_header) = if #name header = "" then SOME "" else NONE;
+
+fun expand_proof thy expand_name prf =
   let
-    fun do_expand a prop =
-      exists (fn (b, NONE) => a = b | (b, SOME prop') => a = b andalso prop = prop') thms;
-
     fun expand seen maxidx (AbsP (s, t, prf)) =
           let val (seen', maxidx', prf') = expand seen maxidx prf
           in (seen', maxidx', AbsP (s, t, prf')) end
@@ -1954,28 +1957,36 @@
       | expand seen maxidx (prf % t) =
           let val (seen', maxidx', prf') = expand seen maxidx prf
           in (seen', maxidx', prf' % t) end
-      | expand seen maxidx (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) =
-          if do_expand a prop then
-            let
-              val (seen', maxidx', prf') =
-                (case AList.lookup (op =) seen (a, prop) of
-                  NONE =>
-                    let
-                      val prf1 =
-                        thm_body_proof_open thm_body
-                        |> reconstruct_proof thy prop
-                        |> forall_intr_vfs_prf prop;
-                      val (seen1, maxidx1, prf2) = expand_init seen prf1
-                      val seen2 = ((a, prop), (maxidx1, prf2)) :: seen1;
-                    in (seen2, maxidx1, prf2) end
-                | SOME (maxidx1, prf1) => (seen, maxidx1, prf1));
-              val prf'' = prf' |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop Ts;
-            in (seen', maxidx' + maxidx + 1, prf'') end
-          else (seen, maxidx, prf)
+      | expand seen maxidx (prf as PThm (header, thm_body)) =
+          let val {serial, pos, theory_name, name, prop, types} = header in
+            (case expand_name header of
+              SOME name' =>
+                if name' = "" andalso is_some types then
+                  let
+                    val (seen', maxidx', prf') =
+                      (case Inttab.lookup seen serial of
+                        NONE =>
+                          let
+                            val prf1 =
+                              thm_body_proof_open thm_body
+                              |> reconstruct_proof thy prop
+                              |> forall_intr_vfs_prf prop;
+                            val (seen1, maxidx1, prf2) = expand_init seen prf1
+                            val seen2 = seen1 |> Inttab.update (serial, (maxidx1, prf2));
+                          in (seen2, maxidx1, prf2) end
+                      | SOME (maxidx1, prf1) => (seen, maxidx1, prf1));
+                    val prf'' = prf'
+                      |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop (the types);
+                  in (seen', maxidx' + maxidx + 1, prf'') end
+                else if name' <> name then
+                  (seen, maxidx, PThm (thm_header serial pos theory_name name' prop types, thm_body))
+                else (seen, maxidx, prf)
+            | NONE => (seen, maxidx, prf))
+          end
       | expand seen maxidx prf = (seen, maxidx, prf)
     and expand_init seen prf = expand seen (maxidx_proof prf ~1) prf;
 
-  in #3 (expand_init [] prf) end;
+  in #3 (expand_init Inttab.empty prf) end;
 
 end;
 
@@ -2289,6 +2300,9 @@
 fun make_thm_id (serial, theory_name) : thm_id =
   {serial = serial, theory_name = theory_name};
 
+fun thm_header_id ({serial, theory_name, ...}: thm_header) =
+  make_thm_id (serial, theory_name);
+
 fun thm_id (serial, thm_node) : thm_id =
   make_thm_id (serial, thm_node_theory_name thm_node);
 

--- a/src/Pure/thm.ML	Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Pure/thm.ML	Sun Oct 20 20:38:22 2019 +0200
@@ -108,6 +108,7 @@
   val derivation_name: thm -> string
   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 close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
@@ -993,6 +994,15 @@
 fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
   Proofterm.get_approximative_name shyps hyps prop (Proofterm.proof_of body);
 
+fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
+  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;
+  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);