# HG changeset patch
# User wenzelm
# Date 1565985057 -7200
# Node ID d18bd904c0fd99450af1532e21bd941e8787dbfb
# Parent  d18195a7c32f4a8f77ce263a048c0a119125b992# Parent  8d7a531a6b58567a5daf230dc4201791d2a7529a
merged

diff -r d18195a7c32f -r d18bd904c0fd src/Pure/facts.ML
--- a/src/Pure/facts.ML	Fri Aug 16 15:48:08 2019 +0100
+++ b/src/Pure/facts.ML	Fri Aug 16 21:50:57 2019 +0200
@@ -46,7 +46,9 @@
   val hide: bool -> string -> T -> T
   type thm_name = string * int
   val thm_name_ord: thm_name * thm_name -> order
-  val single_thm_name: string -> thm_name
+  val thm_name_print: thm_name -> string
+  val thm_name_flat: thm_name -> string
+  val thm_name_list: string -> thm list -> (thm_name * thm) list
   val get_thm: Context.generic -> T -> thm_name * Position.T -> thm
 end;
 
@@ -305,7 +307,16 @@
 type thm_name = string * int;
 val thm_name_ord = prod_ord string_ord int_ord;
 
-fun single_thm_name name : thm_name = (name, 0);
+fun thm_name_print (name, i) =
+  if name = "" orelse i = 0 then name
+  else name ^ enclose "(" ")" (string_of_int i);
+
+fun thm_name_flat (name, i) =
+  if name = "" orelse i = 0 then name
+  else name ^ "_" ^ string_of_int i;
+
+fun thm_name_list name [thm: thm] = [((name, 0), thm)]
+  | thm_name_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;
 
 fun get_thm context facts ((name, i), pos) =
   let
diff -r d18195a7c32f -r d18bd904c0fd src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Aug 16 15:48:08 2019 +0100
+++ b/src/Pure/global_theory.ML	Fri Aug 16 21:50:57 2019 +0200
@@ -12,6 +12,9 @@
   val defined_fact: theory -> string -> bool
   val alias_fact: binding -> string -> theory -> theory
   val hide_fact: bool -> string -> theory -> theory
+  val dest_thms: bool -> theory list -> theory -> (Facts.thm_name * thm) list
+  val dest_thm_names: theory -> (proof_serial * Facts.thm_name) list
+  val lookup_thm_name: theory -> string -> proof_serial -> Facts.thm_name option
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val transfer_theories: theory -> thm -> thm
@@ -19,7 +22,7 @@
   val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
   val burrow_facts: ('a list -> 'b list) ->
     ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
-  val name_multi: string * Position.T -> 'a list -> ((string * Position.T) * 'a) list
+  val name_multi: string * Position.T -> thm list -> ((string * Position.T) * thm) list
   type name_flags
   val unnamed: name_flags
   val official1: name_flags
@@ -55,14 +58,17 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T;
-  val empty = Facts.empty;
-  val extend = I;
-  val merge = Facts.merge;
+  type T = Facts.T * Facts.thm_name Inttab.table lazy option;
+  val empty: T = (Facts.empty, NONE);
+  fun extend (facts, _) = (facts, NONE);
+  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), NONE);
 );
 
-val facts_of = Data.get;
-fun map_facts f = Data.map f;
+
+(* facts *)
+
+val facts_of = #1 o Data.get;
+val map_facts = Data.map o apfst;
 
 fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy);
 val intern_fact = Facts.intern o facts_of;
@@ -73,6 +79,55 @@
 
 fun hide_fact fully name = map_facts (Facts.hide fully name);
 
+fun dest_thms verbose prev_thys thy =
+  Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy)
+  |> maps (uncurry Facts.thm_name_list);
+
+
+(* thm_name vs. derivation_id *)
+
+val thm_names_of = #2 o Data.get;
+val map_thm_names = Data.map o apsnd;
+
+fun make_thm_names thy =
+  (dest_thms true (Theory.parents_of thy) thy, Inttab.empty)
+  |-> fold (fn (thm_name, thm) => fn thm_names =>
+    (case Thm.derivation_id (Thm.transfer thy thm) of
+      NONE => thm_names
+    | SOME {serial, theory_name} =>
+        if Context.theory_long_name thy <> theory_name then
+          raise THM ("Bad theory name for derivation", 0, [thm])
+        else
+          (case Inttab.lookup thm_names serial of
+            SOME thm_name' =>
+              raise THM ("Duplicate use of derivation identity for " ^
+                Facts.thm_name_print thm_name ^ " vs. " ^
+                Facts.thm_name_print thm_name', 0, [thm])
+          | NONE => Inttab.update (serial, thm_name) thm_names)));
+
+fun get_thm_names thy =
+  (case thm_names_of thy of
+    NONE => make_thm_names thy
+  | SOME lazy_tab => Lazy.force lazy_tab);
+
+val dest_thm_names = Inttab.dest o get_thm_names;
+
+fun lookup_thm_name thy theory_name serial =
+  Theory.nodes_of thy |> get_first (fn thy' =>
+    if Context.theory_long_name thy' = theory_name
+    then Inttab.lookup (get_thm_names thy') serial else NONE);
+
+val _ =
+  Theory.setup (Theory.at_end (fn thy =>
+    if is_some (thm_names_of thy) then NONE
+    else
+      let
+        val lazy_tab =
+          if Future.proofs_enabled 1
+          then Lazy.lazy (fn () => make_thm_names thy)
+          else Lazy.value (make_thm_names thy);
+      in SOME (map_thm_names (K (SOME lazy_tab)) thy) end));
+
 
 (* retrieve theorems *)
 
@@ -134,15 +189,11 @@
 
 end;
 
-fun name_multi (name, pos: Position.T) xs =
-  (case xs of
-    [x] => [((name, pos), x)]
-  | _ =>
-      if name = "" then map (pair ("", pos)) xs
-      else map_index (fn (i, x) => ((name ^ "_" ^ string_of_int (i + 1), pos), x)) xs);
+fun name_multi (name, pos) =
+  Facts.thm_name_list name #> (map o apfst) (fn thm_name => (Facts.thm_name_flat thm_name, pos));
 
-fun name_thms name_flags name_pos thms =
-  map (uncurry (name_thm name_flags)) (name_multi name_pos thms);
+fun name_thms name_flags name_pos =
+  name_multi name_pos #> map (uncurry (name_thm name_flags));
 
 
 (* apply theorems and attributes *)
@@ -193,7 +244,8 @@
     in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
 
 val app_facts =
-  apfst flat oo fold_map (fn (thms, atts) => fold_map (Thm.theory_attributes atts) thms);
+  apfst flat oo fold_map (fn (thms, atts) => fn thy =>
+    fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy);
 
 fun apply_facts name_flags1 name_flags2 (b, facts) thy =
   if Binding.is_empty b then app_facts facts thy |-> register_proofs
diff -r d18195a7c32f -r d18bd904c0fd src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Aug 16 15:48:08 2019 +0100
+++ b/src/Pure/proofterm.ML	Fri Aug 16 21:50:57 2019 +0200
@@ -177,6 +177,8 @@
     (string * class list list * class -> proof) -> sort list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
   val get_name: sort list -> term list -> term -> proof -> string
+  val get_id: sort list -> term list -> term -> proof ->
+    {serial: proof_serial, theory_name: string} option
 end
 
 structure Proofterm : PROOFTERM =
@@ -2183,10 +2185,12 @@
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of
-        (PThm ({serial = i, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+        (PThm ({serial, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
           if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
-            let val Thm_Body {body = body', ...} = thm_body';
-            in (i, body' |> (a = "" andalso named) ? Future.map (publish i)) end
+            let
+              val Thm_Body {body = body', ...} = thm_body';
+              val i = if a = "" andalso named then proof_serial () else serial;
+            in (i, body' |> serial <> i ? Future.map (publish i)) end
           else new_prf ()
       | _ => new_prf ());
 
@@ -2221,13 +2225,24 @@
 
 (* approximative PThm name *)
 
-fun get_name shyps hyps prop prf =
+fun get_identity shyps hyps prop prf =
   let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
     (case fst (strip_combt (fst (strip_combP prf))) of
-      PThm ({name, prop = prop', ...}, _) => if prop = prop' then name else ""
-    | _ => "")
+      PThm ({serial, theory_name, name, prop = prop', ...}, _) =>
+        if prop = prop'
+        then SOME {serial = serial, theory_name = theory_name, name = name} else NONE
+    | _ => NONE)
   end;
 
+fun get_name shyps hyps prop prf =
+  Option.map #name (get_identity shyps hyps prop prf) |> the_default "";
+
+fun get_id shyps hyps prop prf =
+  (case get_identity shyps hyps prop prf of
+    NONE => NONE
+  | SOME {name = "", ...} => NONE
+  | SOME {serial, theory_name, ...} => SOME {serial = serial, theory_name = theory_name});
+
 end;
 
 structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
diff -r d18195a7c32f -r d18bd904c0fd src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 16 15:48:08 2019 +0100
+++ b/src/Pure/thm.ML	Fri Aug 16 21:50:57 2019 +0200
@@ -106,6 +106,7 @@
   val future: thm future -> cterm -> thm
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
+  val derivation_id: thm -> {serial: proof_serial, theory_name: string} option
   val raw_derivation_name: thm -> string
   val name_derivation: string * Position.T -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
@@ -1004,6 +1005,9 @@
 fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
   Proofterm.get_name shyps hyps prop (proof_of thm);
 
+fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
+  Proofterm.get_id shyps hyps prop (proof_of thm);
+
 fun name_derivation name_pos =
   solve_constraints #> (fn thm as Thm (der, args) =>
     let