# HG changeset patch
# User paulson
# Date 1565956427 -3600
# Node ID 87dffe9700bdfc984ed7f8b1980260501a958396
# Parent  2970fdc230cc2d292dbe2fad94df4df019103b4b# Parent  7ce95a5c4aa86a7dca5a292778f96af978109094
merged

diff -r 7ce95a5c4aa8 -r 87dffe9700bd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Aug 16 12:53:47 2019 +0100
@@ -282,7 +282,7 @@
         val atts = map (attribute_generic context) srcs;
         val (ths', context') =
           fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
-      in (context', pick (name, Facts.pos_of_ref thmref) ths') end)
+      in (context', pick (name, Facts.ref_pos thmref) ths') end)
   end);
 
 in
diff -r 7ce95a5c4aa8 -r 87dffe9700bd src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/Isar/generic_target.ML	Fri Aug 16 12:53:47 2019 +0100
@@ -306,6 +306,8 @@
 fun bind_name lthy b =
   (Local_Theory.full_name lthy b, Binding.default_pos_of b);
 
+fun map_facts f = map (apsnd (map (apfst (map f))));
+
 in
 
 fun notes target_notes kind facts lthy =
@@ -313,9 +315,9 @@
     val facts' = facts
       |> map (fn (a, bs) =>
           (a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs))
-      |> Global_Theory.map_facts (import_export_proof lthy);
-    val local_facts = Global_Theory.map_facts #1 facts';
-    val global_facts = Global_Theory.map_facts #2 facts';
+      |> map_facts (import_export_proof lthy);
+    val local_facts = map_facts #1 facts';
+    val global_facts = map_facts #2 facts';
   in
     lthy
     |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
diff -r 7ce95a5c4aa8 -r 87dffe9700bd src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 16 12:53:47 2019 +0100
@@ -125,7 +125,7 @@
 (* filter_name *)
 
 fun filter_name str_pat (thmref, _) =
-  if match_string str_pat (Facts.name_of_ref thmref)
+  if match_string str_pat (Facts.ref_name thmref)
   then SOME (0, 0, 0) else NONE;
 
 
diff -r 7ce95a5c4aa8 -r 87dffe9700bd src/Pure/facts.ML
--- a/src/Pure/facts.ML	Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/facts.ML	Fri Aug 16 12:53:47 2019 +0100
@@ -12,11 +12,11 @@
     Named of (string * Position.T) * interval list option |
     Fact of string
   val named: string -> ref
+  val ref_name: ref -> string
+  val ref_pos: ref -> Position.T
+  val map_ref_name: (string -> string) -> ref -> ref
   val string_of_selection: interval list option -> string
   val string_of_ref: ref -> string
-  val name_of_ref: ref -> string
-  val pos_of_ref: ref -> Position.T
-  val map_name_of_ref: (string -> string) -> ref -> ref
   val select: ref -> thm list -> thm list
   val selections: string * thm list -> (ref * thm) list
   type T
@@ -44,6 +44,10 @@
   val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   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 get_thm: Context.generic -> T -> thm_name * Position.T -> thm
 end;
 
 structure Facts: FACTS =
@@ -51,10 +55,18 @@
 
 (** fact references **)
 
-fun the_single _ [th] : thm = th
-  | the_single (name, pos) ths =
-      error ("Expected singleton fact " ^ quote name ^
-        " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
+fun length_msg (thms: thm list) pos =
+  " (length " ^ string_of_int (length thms) ^ ")" ^ Position.here pos;
+
+fun err_single (name, pos) thms =
+  error ("Expected singleton fact " ^ quote name ^ length_msg thms pos);
+
+fun err_selection (name, pos) i thms =
+  error ("Bad fact selection " ^ quote (name ^ enclose "(" ")" (string_of_int i)) ^
+    length_msg thms pos);
+
+fun the_single _ [thm] = thm
+  | the_single name_pos thms = err_single name_pos thms;
 
 
 (* datatype interval *)
@@ -85,14 +97,14 @@
 
 fun named name = Named ((name, Position.none), NONE);
 
-fun name_of_ref (Named ((name, _), _)) = name
-  | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
+fun ref_name (Named ((name, _), _)) = name
+  | ref_name (Fact _) = raise Fail "Illegal literal fact";
 
-fun pos_of_ref (Named ((_, pos), _)) = pos
-  | pos_of_ref (Fact _) = Position.none;
+fun ref_pos (Named ((_, pos), _)) = pos
+  | ref_pos (Fact _) = Position.none;
 
-fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
-  | map_name_of_ref _ r = r;
+fun map_ref_name f (Named ((name, pos), is)) = Named ((f name, pos), is)
+  | map_ref_name _ r = r;
 
 fun string_of_selection NONE = ""
   | string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is));
@@ -108,12 +120,10 @@
   | select (Named ((name, pos), SOME ivs)) ths =
       let
         val n = length ths;
-        fun err msg =
-          error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
-            Position.here pos);
+        fun err msg = error (msg ^ " for fact " ^ quote name ^ length_msg ths pos);
         fun sel i =
-          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
-          else nth ths (i - 1);
+          if i > 0 andalso i <= n then nth ths (i - 1)
+          else err_selection (name, pos) i ths;
         val is = maps (interval n) ivs handle Fail msg => err msg;
       in map sel is end;
 
@@ -288,4 +298,27 @@
 fun hide fully name (Facts {facts, props}) =
   make_facts (Name_Space.hide_table fully name facts) props;
 
+
+
+(** get individual theorems **)
+
+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 get_thm context facts ((name, i), pos) =
+  let
+    fun print_name () =
+      markup_extern (Context.proof_of context) facts name |-> Markup.markup;
+  in
+    (case (lookup context facts name, i) of
+      (NONE, _) => error ("Undefined fact " ^ quote (print_name ()) ^ Position.here pos)
+    | (SOME {thms = [thm], ...}, 0) => thm
+    | (SOME {thms, ...}, 0) => err_single (print_name (), pos) thms
+    | (SOME {thms, ...}, _) =>
+        if i > 0 andalso i <= length thms then nth thms (i - 1)
+        else err_selection (print_name (), pos) i thms)
+  end;
+
 end;
diff -r 7ce95a5c4aa8 -r 87dffe9700bd src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/global_theory.ML	Fri Aug 16 12:53:47 2019 +0100
@@ -16,7 +16,6 @@
   val get_thm: theory -> xstring -> thm
   val transfer_theories: theory -> thm -> thm
   val all_thms_of: theory -> bool -> (string * thm) list
-  val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   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
@@ -63,15 +62,16 @@
 );
 
 val facts_of = Data.get;
+fun map_facts f = Data.map f;
 
 fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy);
 val intern_fact = Facts.intern o facts_of;
 val defined_fact = Facts.defined o facts_of;
 
 fun alias_fact binding name thy =
-  Data.map (Facts.alias (Sign.naming_of thy) binding name) thy;
+  map_facts (Facts.alias (Sign.naming_of thy) binding name) thy;
 
-fun hide_fact fully name = Data.map (Facts.hide fully name);
+fun hide_fact fully name = map_facts (Facts.hide fully name);
 
 
 (* retrieve theorems *)
@@ -106,7 +106,6 @@
 
 (* fact specifications *)
 
-fun map_facts f = map (apsnd (map (apfst (map f))));
 fun burrow_fact f = split_list #>> burrow f #> op ~~;
 fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
 
@@ -128,7 +127,7 @@
       No_Name_Flags => thm
     | Name_Flags {pre, official} =>
         thm
-        |> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
+        |> (official andalso (not pre orelse Thm.raw_derivation_name thm = "")) ?
             Thm.name_derivation (name, pos)
         |> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
             Thm.put_name_hint name));
@@ -176,7 +175,7 @@
         end);
     val arg = (b, Lazy.map_finished (tap check) fact);
   in
-    thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
+    thy |> map_facts (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
   end;
 
 fun check_thms_lazy (thms: thm list lazy) =
@@ -231,8 +230,8 @@
 (* dynamic theorems *)
 
 fun add_thms_dynamic' context arg thy =
-  let val (name, facts') = Facts.add_dynamic context arg (Data.get thy)
-  in (name, Data.put facts' thy) end;
+  let val (name, facts') = Facts.add_dynamic context arg (facts_of thy)
+  in (name, map_facts (K facts') thy) end;
 
 fun add_thms_dynamic arg thy =
   add_thms_dynamic' (Context.Theory thy) arg thy |> snd;
diff -r 7ce95a5c4aa8 -r 87dffe9700bd src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/thm.ML	Fri Aug 16 12:53:47 2019 +0100
@@ -106,6 +106,7 @@
   val future: thm future -> cterm -> thm
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
+  val raw_derivation_name: thm -> string
   val name_derivation: string * Position.T -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
@@ -996,9 +997,13 @@
   Proofterm.compact_proof (Proofterm.proof_of body);
 
 (*non-deterministic, depends on unknown promises*)
-fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
+fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
   Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
 
+(*deterministic name of finished proof*)
+fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
+  Proofterm.get_name shyps hyps prop (proof_of thm);
+
 fun name_derivation name_pos =
   solve_constraints #> (fn thm as Thm (der, args) =>
     let