# HG changeset patch
# User wenzelm
# Date 1566243454 -7200
# Node ID ea860617fac193bcbf7223d35cf4b900e375c9e0
# Parent  b63e5e4598d7465998bb90a6639f18195d3f00f5# Parent  e6101f131d0d75987bad539a51083e8759db4306
merged

diff -r b63e5e4598d7 -r ea860617fac1 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Aug 19 21:37:34 2019 +0200
@@ -622,7 +622,7 @@
                     val corr_prf = mkabsp shyps corr_prf0;
                     val corr_prop = Proofterm.prop_of corr_prf;
                     val corr_header =
-                      Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
+                      Proofterm.thm_header (serial ()) pos theory_name
                         (corr_name name vs') corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf);
@@ -743,7 +743,7 @@
                              SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
                     val corr_prop = Proofterm.prop_of corr_prf';
                     val corr_header =
-                      Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
+                      Proofterm.thm_header (serial ()) pos theory_name
                         (corr_name s vs') corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf');
diff -r b63e5e4598d7 -r ea860617fac1 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 19 21:37:34 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 b63e5e4598d7 -r ea860617fac1 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Mon Aug 19 21:37:34 2019 +0200
@@ -218,7 +218,7 @@
         (#constants (Consts.dest (Sign.consts_of thy)));
 
 
-    (* axioms and facts *)
+    (* axioms *)
 
     fun standard_prop used extra_shyps raw_prop raw_proof =
       let
@@ -236,12 +236,26 @@
     fun encode_axiom used prop =
       encode_prop (#1 (standard_prop used [] prop NONE));
 
+    val _ =
+      export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
+        Theory.axiom_space (Theory.axioms_of thy);
+
+
+    (* theorems *)
+
     val clean_thm =
       Thm.transfer thy
       #> Thm.check_hyps (Context.Theory thy)
       #> Thm.strip_shyps;
 
-    val encode_fact = clean_thm #> (fn thm =>
+    fun entity_markup_thm (serial, (name, i)) =
+      let
+        val space = Facts.space_of (Global_Theory.facts_of thy);
+        val xname = Name_Space.extern_shortest thy_ctxt space name;
+        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;
+
+    val encode_thm = clean_thm #> (fn thm =>
       standard_prop Name.context
         (Thm.extra_shyps thm)
         (Thm.full_prop_of thm)
@@ -249,13 +263,16 @@
       let open XML.Encode Term_XML.Encode
       in pair encode_prop (option Proofterm.encode_full) end);
 
-    val _ =
-      export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
-        Theory.axiom_space (Theory.axioms_of thy);
-    val _ =
-      export_entities "facts" (K (SOME o XML.Encode.list encode_fact))
-        (Facts.space_of o Global_Theory.facts_of)
-        (Facts.dest_static true [] (Global_Theory.facts_of thy));
+    fun export_thms thms =
+      let val elems =
+        thms |> map (fn (serial, thm_name) =>
+          let
+            val markup = entity_markup_thm (serial, thm_name);
+            val body = encode_thm (Global_Theory.get_thm_name thy (thm_name, Position.none));
+          in XML.Elem (markup, body) end)
+      in if null elems then () else export_body thy "thms" elems end;
+
+    val _ = export_thms (Global_Theory.dest_thm_names thy);
 
 
     (* type classes *)
diff -r b63e5e4598d7 -r ea860617fac1 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Mon Aug 19 21:37:34 2019 +0200
@@ -28,7 +28,7 @@
     types: Boolean = true,
     consts: Boolean = true,
     axioms: Boolean = true,
-    facts: Boolean = true,
+    thms: Boolean = true,
     classes: Boolean = true,
     locales: Boolean = true,
     locale_dependencies: Boolean = true,
@@ -44,7 +44,7 @@
           Export.read_theory_names(db, session_name).map((theory_name: String) =>
             read_theory(Export.Provider.database(db, session_name, theory_name),
               session_name, theory_name, types = types, consts = consts,
-              axioms = axioms, facts = facts, classes = classes, locales = locales,
+              axioms = axioms, thms = thms, classes = classes, locales = locales,
               locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
               typedefs = typedefs, cache = Some(cache)))
         }
@@ -70,8 +70,8 @@
   sealed case class Theory(name: String, parents: List[String],
     types: List[Type],
     consts: List[Const],
-    axioms: List[Fact_Single],
-    facts: List[Fact_Multi],
+    axioms: List[Axiom],
+    thms: List[Thm],
     classes: List[Class],
     locales: List[Locale],
     locale_dependencies: List[Locale_Dependency],
@@ -86,7 +86,7 @@
         types.iterator.map(_.entity.serial) ++
         consts.iterator.map(_.entity.serial) ++
         axioms.iterator.map(_.entity.serial) ++
-        facts.iterator.map(_.entity.serial) ++
+        thms.iterator.map(_.entity.serial) ++
         classes.iterator.map(_.entity.serial) ++
         locales.iterator.map(_.entity.serial) ++
         locale_dependencies.iterator.map(_.entity.serial)
@@ -97,7 +97,7 @@
         types.map(_.cache(cache)),
         consts.map(_.cache(cache)),
         axioms.map(_.cache(cache)),
-        facts.map(_.cache(cache)),
+        thms.map(_.cache(cache)),
         classes.map(_.cache(cache)),
         locales.map(_.cache(cache)),
         locale_dependencies.map(_.cache(cache)),
@@ -113,7 +113,7 @@
     types: Boolean = true,
     consts: Boolean = true,
     axioms: Boolean = true,
-    facts: Boolean = true,
+    thms: Boolean = true,
     classes: Boolean = true,
     locales: Boolean = true,
     locale_dependencies: Boolean = true,
@@ -134,7 +134,7 @@
         if (types) read_types(provider) else Nil,
         if (consts) read_consts(provider) else Nil,
         if (axioms) read_axioms(provider) else Nil,
-        if (facts) read_facts(provider) else Nil,
+        if (thms) read_thms(provider) else Nil,
         if (classes) read_classes(provider) else Nil,
         if (locales) read_locales(provider) else Nil,
         if (locale_dependencies) read_locale_dependencies(provider) else Nil,
@@ -166,7 +166,7 @@
     val TYPE = Value("type")
     val CONST = Value("const")
     val AXIOM = Value("axiom")
-    val FACT = Value("fact")
+    val THM = Value("thm")
     val CLASS = Value("class")
     val LOCALE = Value("locale")
     val LOCALE_DEPENDENCY = Value("locale_dependency")
@@ -285,7 +285,7 @@
       })
 
 
-  /* axioms and facts */
+  /* axioms */
 
   sealed case class Prop(
     typargs: List[(String, Term.Sort)],
@@ -310,62 +310,40 @@
     Prop(typargs, args, t)
   }
 
-
-  sealed case class Fact(prop: Prop, proof: Option[Term.Proof])
+  sealed case class Axiom(entity: Entity, prop: Prop)
   {
-    def cache(cache: Term.Cache): Fact =
-      Fact(prop.cache(cache), proof.map(cache.proof _))
-  }
-
-  def decode_fact(body: XML.Body): Fact =
-  {
-    val (prop, proof) =
-    {
-      import XML.Decode._
-      pair(decode_prop _, option(Term_XML.Decode.proof))(body)
-    }
-    Fact(prop, proof)
+    def cache(cache: Term.Cache): Axiom =
+      Axiom(entity.cache(cache), prop.cache(cache))
   }
 
-  sealed case class Fact_Single(entity: Entity, fact: Fact)
-  {
-    def cache(cache: Term.Cache): Fact_Single =
-      Fact_Single(entity.cache(cache), fact.cache(cache))
-
-    def prop: Prop = fact.prop
-    def proof: Option[Term.Proof] = fact.proof
-  }
-
-  sealed case class Fact_Multi(entity: Entity, facts: List[Fact])
-  {
-    def cache(cache: Term.Cache): Fact_Multi =
-      Fact_Multi(entity.cache(cache), facts.map(_.cache(cache)))
-
-    def props: List[Prop] = facts.map(_.prop)
-
-    def split: List[Fact_Single] =
-      facts match {
-        case List(fact) => List(Fact_Single(entity, fact))
-        case _ =>
-          for ((fact, i) <- facts.zipWithIndex)
-          yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), fact)
-      }
-  }
-
-  def read_axioms(provider: Export.Provider): List[Fact_Single] =
+  def read_axioms(provider: Export.Provider): List[Axiom] =
     provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.AXIOM, tree)
         val prop = decode_prop(body)
-        Fact_Single(entity, Fact(prop, None))
+        Axiom(entity, prop)
       })
 
-  def read_facts(provider: Export.Provider): List[Fact_Multi] =
-    provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
+
+  /* theorems */
+
+  sealed case class Thm(entity: Entity, prop: Prop, proof: Option[Term.Proof])
+  {
+    def cache(cache: Term.Cache): Thm =
+      Thm(entity.cache(cache), prop.cache(cache), proof.map(cache.proof _))
+  }
+
+  def read_thms(provider: Export.Provider): List[Thm] =
+    provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
       {
-        val (entity, body) = decode_entity(Kind.FACT, tree)
-        val facts = XML.Decode.list(decode_fact)(body)
-        Fact_Multi(entity, facts)
+        val (entity, body) = decode_entity(Kind.THM, tree)
+        val (prop, prf) =
+        {
+          import XML.Decode._
+          import Term_XML.Decode._
+          pair(decode_prop _, option(proof))(body)
+        }
+        Thm(entity, prop, prf)
       })
 
   def read_proof(
diff -r b63e5e4598d7 -r ea860617fac1 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/build-jars	Mon Aug 19 21:37:34 2019 +0200
@@ -171,6 +171,7 @@
   pure_thy.scala
   term.scala
   term_xml.scala
+  thm_name.scala
   ../Tools/Graphview/graph_file.scala
   ../Tools/Graphview/graph_panel.scala
   ../Tools/Graphview/graphview.scala
diff -r b63e5e4598d7 -r ea860617fac1 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/facts.ML	Mon Aug 19 21:37:34 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 b63e5e4598d7 -r ea860617fac1 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/global_theory.ML	Mon Aug 19 21:37:34 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 -> (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 b63e5e4598d7 -r ea860617fac1 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Aug 19 21:37:34 2019 +0200
@@ -6,12 +6,11 @@
 
 infix 8 % %% %>;
 
-signature BASIC_PROOFTERM =
+signature PROOFTERM =
 sig
   type thm_node
-  type proof_serial = int
   type thm_header =
-    {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
+    {serial: serial, pos: Position.T list, theory_name: string, name: string,
       prop: term, types: typ list option}
   type thm_body
   datatype proof =
@@ -28,21 +27,16 @@
    | PThm of thm_header * thm_body
   and proof_body = PBody of
     {oracles: (string * term option) Ord_List.T,
-     thms: (proof_serial * thm_node) Ord_List.T,
+     thms: (serial * thm_node) Ord_List.T,
      proof: proof}
   val %> : proof * term -> proof
-end;
-
-signature PROOFTERM =
-sig
-  include BASIC_PROOFTERM
   val proofs: int Unsynchronized.ref
   exception MIN_PROOF
-  type pthm = proof_serial * thm_node
+  type pthm = serial * thm_node
   type oracle = string * term option
   val proof_of: proof_body -> proof
   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
-  val thm_header: proof_serial -> Position.T list -> string -> string -> term -> typ list option ->
+  val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option ->
     thm_header
   val thm_body: proof_body -> thm_body
   val thm_body_proof_raw: thm_body -> proof
@@ -53,7 +47,7 @@
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms:
-    ({serial: proof_serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
+    ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
     proof_body list -> 'a -> 'a
   val consolidate: proof_body list -> unit
 
@@ -168,7 +162,6 @@
   val standard_vars: Name.context -> term * proof option -> term * proof option
   val standard_vars_term: Name.context -> term -> term
 
-  val proof_serial: unit -> proof_serial
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> string * Position.T -> sort list ->
@@ -177,7 +170,7 @@
     (string * class list list * class -> proof) -> sort list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
   val get_approximative_name: sort list -> term list -> term -> proof -> string
-  type thm_id = {serial: proof_serial, theory_name: string}
+  type thm_id = {serial: serial, theory_name: string}
   val get_id: sort list -> term list -> term -> proof -> thm_id option
 end
 
@@ -186,10 +179,8 @@
 
 (** datatype proof **)
 
-type proof_serial = int;
-
 type thm_header =
-  {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
+  {serial: serial, pos: Position.T list, theory_name: string, name: string,
     prop: term, types: typ list option};
 
 datatype proof =
@@ -206,7 +197,7 @@
  | PThm of thm_header * thm_body
 and proof_body = PBody of
   {oracles: (string * term option) Ord_List.T,
-   thms: (proof_serial * thm_node) Ord_List.T,
+   thms: (serial * thm_node) Ord_List.T,
    proof: proof}
 and thm_body =
   Thm_Body of {export_proof: unit lazy, open_proof: proof -> proof, body: proof_body future}
@@ -218,7 +209,7 @@
 type oracle = string * term option;
 val oracle_prop = the_default Term.dummy;
 
-type pthm = proof_serial * thm_node;
+type pthm = serial * thm_node;
 
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
@@ -302,11 +293,11 @@
   let
     fun collect (PBody {oracles, thms, ...}) =
       (if null oracles then I else apfst (cons oracles)) #>
-      (tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
-        if Inttab.defined seen i then (x, seen)
+      (tap join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
+        if Inttab.defined seen i then (res, seen)
         else
           let val body = Future.join (thm_node_body thm_node)
-          in collect body (x, Inttab.update (i, ()) seen) end));
+          in collect body (res, Inttab.update (i, ()) seen) end));
   in fold collect bodies ([], Inttab.empty) |> #1 |> unions_oracles end;
 
 fun approximate_proof_body prf =
@@ -2067,8 +2058,6 @@
 
 (* PThm nodes *)
 
-val proof_serial = Counter.make ();
-
 local
 
 fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) =
@@ -2156,7 +2145,7 @@
 
     fun new_prf () =
       let
-        val i = proof_serial ();
+        val i = serial ();
         val unconstrainT =
           unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
         val postproc = map_proof_of unconstrainT #> named ? publish i;
@@ -2165,12 +2154,12 @@
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of
-        (PThm ({serial, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+        (PThm ({serial = ser, 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';
-              val i = if a = "" andalso named then proof_serial () else serial;
-            in (i, body' |> serial <> i ? Future.map (publish i)) end
+              val i = if a = "" andalso named then serial () else ser;
+            in (i, body' |> ser <> i ? Future.map (publish i)) end
           else new_prf ()
       | _ => new_prf ());
 
@@ -2218,7 +2207,7 @@
   Option.map #name (get_identity shyps hyps prop prf) |> the_default "";
 
 
-type thm_id = {serial: proof_serial, theory_name: string};
+type thm_id = {serial: serial, theory_name: string};
 
 fun get_id shyps hyps prop prf : thm_id option =
   (case get_identity shyps hyps prop prf of
@@ -2228,5 +2217,11 @@
 
 end;
 
-structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
+structure Basic_Proofterm =
+struct
+  datatype proof = datatype Proofterm.proof
+  datatype proof_body = datatype Proofterm.proof_body
+  val op %> = Proofterm.%>
+end;
+
 open Basic_Proofterm;
diff -r b63e5e4598d7 -r ea860617fac1 src/Pure/thm_name.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/thm_name.ML	Mon Aug 19 21:37:34 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, index) =
+  if name = "" orelse index = 0 then name
+  else name ^ enclose "(" ")" (string_of_int index);
+
+fun flatten (name, index) =
+  if name = "" orelse index = 0 then name
+  else name ^ "_" ^ string_of_int index;
+
+fun make_list name [thm: thm] = [((name, 0), thm)]
+  | make_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;
+
+end;
diff -r b63e5e4598d7 -r ea860617fac1 src/Pure/thm_name.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/thm_name.scala	Mon Aug 19 21:37:34 2019 +0200
@@ -0,0 +1,44 @@
+/*  Title:      Pure/thm_name.scala
+    Author:     Makarius
+
+Systematic naming of individual theorems, as selections from multi-facts.
+*/
+
+package isabelle
+
+
+import scala.math.Ordering
+
+
+object Thm_Name
+{
+  object Ordering extends scala.math.Ordering[Thm_Name]
+  {
+    def compare(thm_name1: Thm_Name, thm_name2: Thm_Name): Int =
+      thm_name1.name compare thm_name2.name match {
+        case 0 => thm_name1.index compare thm_name2.index
+        case ord => ord
+      }
+  }
+
+  def graph[A]: Graph[Thm_Name, A] = Graph.empty(Ordering)
+
+  private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r
+
+  def parse(s: String): Thm_Name =
+    s match {
+      case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
+      case _ => Thm_Name(s, 0)
+    }
+}
+
+sealed case class Thm_Name(name: String, index: Int)
+{
+  def print: String =
+    if (name == "" || index == 0) name
+    else name + "(" + index + ")"
+
+  def flatten: String =
+    if (name == "" || index == 0) name
+    else name + "_" + index
+}