# HG changeset patch
# User wenzelm
# Date 1566234764 -7200
# Node ID 503ca64329cc7557a7f134456f90d3b7309aa522
# Parent  10dd61d9357a87a040cd41ff035f7cf1e287595f
clarified modules;

diff -r 10dd61d9357a -r 503ca64329cc src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Aug 19 18:47:49 2019 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 19 19:12:44 2019 +0200
@@ -175,6 +175,7 @@
 ML_file "more_thm.ML";
 
 ML_file "facts.ML";
+ML_file "thm_name.ML";
 ML_file "global_theory.ML";
 ML_file "pure_thy.ML";
 ML_file "drule.ML";
diff -r 10dd61d9357a -r 503ca64329cc src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Aug 19 18:47:49 2019 +0200
+++ b/src/Pure/facts.ML	Mon Aug 19 19:12:44 2019 +0200
@@ -6,6 +6,8 @@
 
 signature FACTS =
 sig
+  val err_selection: string * Position.T -> int -> thm list -> 'a
+  val err_single: string * Position.T -> thm list -> 'a
   val the_single: string * Position.T -> thm list -> thm
   datatype interval = FromTo of int * int | From of int | Single of int
   datatype ref =
@@ -44,12 +46,6 @@
   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 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;
 
 structure Facts: FACTS =
@@ -60,13 +56,13 @@
 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 err_single (name, pos) thms =
+  error ("Expected singleton fact " ^ quote name ^ length_msg thms pos);
+
 fun the_single _ [thm] = thm
   | the_single name_pos thms = err_single name_pos thms;
 
@@ -300,36 +296,4 @@
 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 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
-    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 10dd61d9357a -r 503ca64329cc src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Mon Aug 19 18:47:49 2019 +0200
+++ b/src/Pure/global_theory.ML	Mon Aug 19 19:12:44 2019 +0200
@@ -12,14 +12,15 @@
   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_id: theory -> Proofterm.thm_id -> Facts.thm_name option
-  val lookup_thm: theory -> thm -> Facts.thm_name option
+  val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
+  val dest_thm_names: theory -> (proof_serial * Thm_Name.T) list
+  val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
+  val lookup_thm: theory -> thm -> Thm_Name.T option
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val transfer_theories: theory -> thm -> thm
   val all_thms_of: theory -> bool -> (string * thm) list
+  val get_thm_name: theory -> Thm_Name.T * Position.T -> thm
   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
@@ -59,7 +60,7 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T * Facts.thm_name Inttab.table lazy option;
+  type T = Facts.T * Thm_Name.T Inttab.table lazy option;
   val empty: T = (Facts.empty, NONE);
   fun extend (facts, _) = (facts, NONE);
   fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), NONE);
@@ -82,7 +83,7 @@
 
 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);
+  |> maps (uncurry Thm_Name.make_list);
 
 
 (* thm_name vs. derivation_id *)
@@ -102,8 +103,8 @@
           (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])
+                Thm_Name.print thm_name ^ " vs. " ^
+                Thm_Name.print thm_name', 0, [thm])
           | NONE => Inttab.update (serial, thm_name) thm_names)));
 
 fun get_thm_names thy =
@@ -166,6 +167,21 @@
       else append (map (`(Thm.get_name_hint) o transfer) ths);
   in Facts.fold_static add facts [] end;
 
+fun get_thm_name thy ((name, i), pos) =
+  let
+    val facts = facts_of thy;
+    fun print_name () =
+      Facts.markup_extern (Proof_Context.init_global thy) facts name |-> Markup.markup;
+  in
+    (case (Facts.lookup (Context.Theory thy) facts name, i) of
+      (NONE, _) => error ("Undefined fact " ^ quote (print_name ()) ^ Position.here pos)
+    | (SOME {thms = [thm], ...}, 0) => thm
+    | (SOME {thms, ...}, 0) => Facts.err_single (print_name (), pos) thms
+    | (SOME {thms, ...}, _) =>
+        if i > 0 andalso i <= length thms then nth thms (i - 1)
+        else Facts.err_selection (print_name (), pos) i thms)
+  end;
+
 
 
 (** store theorems **)
@@ -201,7 +217,7 @@
 end;
 
 fun name_multi (name, pos) =
-  Facts.thm_name_list name #> (map o apfst) (fn thm_name => (Facts.thm_name_flat thm_name, pos));
+  Thm_Name.make_list name #> (map o apfst) (fn thm_name => (Thm_Name.flatten thm_name, pos));
 
 fun name_thms name_flags name_pos =
   name_multi name_pos #> map (uncurry (name_thm name_flags));
diff -r 10dd61d9357a -r 503ca64329cc src/Pure/thm_name.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/thm_name.ML	Mon Aug 19 19:12:44 2019 +0200
@@ -0,0 +1,36 @@
+(*  Title:      Pure/thm_name.ML
+    Author:     Makarius
+
+Systematic naming of individual theorems, as selections from multi-facts.
+
+  (NAME, 0): the single entry of a singleton fact NAME
+  (NAME, i): entry i of a non-singleton fact (1 <= i <= length)
+*)
+
+signature THM_NAME =
+sig
+  type T = string * int
+  val ord: T * T -> order
+  val print: T -> string
+  val flatten: T -> string
+  val make_list: string -> thm list -> (T * thm) list
+end;
+
+structure Thm_Name: THM_NAME =
+struct
+
+type T = string * int;
+val ord = prod_ord string_ord int_ord;
+
+fun print (name, i) =
+  if name = "" orelse i = 0 then name
+  else name ^ enclose "(" ")" (string_of_int i);
+
+fun flatten (name, i) =
+  if name = "" orelse i = 0 then name
+  else name ^ "_" ^ string_of_int i;
+
+fun make_list name [thm: thm] = [((name, 0), thm)]
+  | make_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;
+
+end;