clarified PThm: theory_name simplifies retrieval from exports;

--- a/src/Pure/Proof/extraction.ML	Thu Aug 15 16:38:55 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Aug 15 16:57:09 2019 +0200
@@ -597,7 +597,7 @@
 
       | corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
           let
-            val {pos, name, prop, ...} = thm_header;
+            val {pos, theory_name, name, prop, ...} = thm_header;
             val prf = Proofterm.thm_body_proof_open thm_body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
@@ -622,8 +622,9 @@
                     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 (corr_name name vs')
-                        corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
+                      Proofterm.thm_header (Proofterm.proof_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);
                     val corr_prf' =
                       Proofterm.proof_combP
@@ -698,7 +699,7 @@
 
       | extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
           let
-            val {pos, name = s, prop, ...} = thm_header;
+            val {pos, theory_name, name = s, prop, ...} = thm_header;
             val prf = Proofterm.thm_body_proof_open thm_body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
@@ -742,8 +743,9 @@
                              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 (corr_name s vs')
-                        corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
+                      Proofterm.thm_header (Proofterm.proof_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');
                     val corr_prf'' =
                       Proofterm.proof_combP (Proofterm.proof_combt

--- a/src/Pure/proofterm.ML	Thu Aug 15 16:38:55 2019 +0200
+++ b/src/Pure/proofterm.ML	Thu Aug 15 16:57:09 2019 +0200
@@ -11,7 +11,8 @@
   type thm_node
   type proof_serial = int
   type thm_header =
-    {serial: proof_serial, pos: Position.T list, name: string, prop: term, types: typ list option}
+    {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
+      prop: term, types: typ list option}
   type thm_body
   datatype proof =
      MinProof
@@ -40,7 +41,8 @@
   type oracle = string * term
   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 -> term -> typ list option -> thm_header
+  val thm_header: proof_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
   val thm_body_proof_open: thm_body -> proof
@@ -189,7 +191,8 @@
 type proof_serial = int;
 
 type thm_header =
-  {serial: proof_serial, pos: Position.T list, name: string, prop: term, types: typ list option};
+  {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
+    prop: term, types: typ list option};
 
 datatype proof =
    MinProof
@@ -221,8 +224,8 @@
 fun map_proof_of f (PBody {oracles, thms, proof}) =
   PBody {oracles = oracles, thms = thms, proof = f proof};
 
-fun thm_header serial pos name prop types : thm_header =
-  {serial = serial, pos = pos, name = name, prop = prop, types = types};
+fun thm_header serial pos theory_name name prop types : thm_header =
+  {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
 
 val no_export_proof = Lazy.value ();
 
@@ -383,8 +386,8 @@
   fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
   fn OfClass (a, b) => ([b], typ a),
   fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
-  fn PThm ({serial, pos, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
-    ([int_atom serial, name],
+  fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
+    ([int_atom serial, theory_name, name],
       pair (list properties) (pair term (pair (option (list typ)) proof_body))
         (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
 and proof_body (PBody {oracles, thms, proof = prf}) =
@@ -404,7 +407,8 @@
   fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
   fn OfClass (T, c) => ([c], typ T),
   fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
-  fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
+  fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
+    ([int_atom serial, theory_name, name], list typ Ts)];
 
 in
 
@@ -432,12 +436,12 @@
   fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end,
   fn ([b], a) => OfClass (typ a, b),
   fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
-  fn ([a, b], c) =>
+  fn ([a, b, c], d) =>
     let
-      val ((d, (e, (f, g)))) =
-        pair (list properties) (pair term (pair (option (list typ)) proof_body)) c;
-      val header = thm_header (int_atom a) (map Position.of_properties d) b e f;
-    in PThm (header, thm_body g) end]
+      val ((e, (f, (g, h)))) =
+        pair (list properties) (pair term (pair (option (list typ)) proof_body)) d;
+      val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
+    in PThm (header, thm_body h) end]
 and proof_body x =
   let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
   in PBody {oracles = a, thms = b, proof = c} end
@@ -511,8 +515,8 @@
       | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
       | proof (OfClass T_c) = ofclass T_c
       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
-      | proof (PThm ({serial, pos, name, prop, types = SOME Ts}, thm_body)) =
-          PThm (thm_header serial pos name prop (SOME (typs Ts)), thm_body)
+      | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) =
+          PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
       | proof _ = raise Same.SAME;
   in proof end;
 
@@ -551,8 +555,8 @@
 fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
   | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
   | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
-  | change_types types (PThm ({serial, pos, name, prop, types = _}, thm_body)) =
-      PThm (thm_header serial pos name prop types, thm_body)
+  | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) =
+      PThm (thm_header serial pos theory_name name prop types, thm_body)
   | change_types _ prf = prf;
 
 
@@ -699,8 +703,9 @@
           OfClass (htypeT Envir.norm_type_same T, c)
       | norm (Oracle (s, prop, Ts)) =
           Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
-      | norm (PThm ({serial = i, pos = p, name = a, prop = t, types = Ts}, thm_body)) =
-          PThm (thm_header i p a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
+      | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
+          PThm (thm_header i p theory_name a t
+            (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
       | norm _ = raise Same.SAME;
   in Same.commit norm end;
 
@@ -1016,9 +1021,9 @@
           OfClass (Logic.incr_tvar_same inc T, c)
       | lift' _ _ (Oracle (s, prop, Ts)) =
           Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
-      | lift' _ _ (PThm ({serial = i, pos = p, name = s, prop, types = Ts}, thm_body)) =
-          PThm (thm_header i p s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts),
-            thm_body)
+      | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) =
+          PThm (thm_header i p theory_name s prop
+            ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body)
       | lift' _ _ _ = raise Same.SAME
     and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
 
@@ -1447,8 +1452,8 @@
       | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
       | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
       | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
-      | subst _ _ (PThm ({serial = i, pos = p, name = id, prop, types}, thm_body)) =
-          PThm (thm_header i p id prop (Same.map_option substTs types), thm_body)
+      | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) =
+          PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
       | subst _ _ _ = raise Same.SAME;
   in fn t => subst 0 0 t handle Same.SAME => t end;
 
@@ -2189,7 +2194,8 @@
 
     val pthm = (i, make_thm_node name prop1 body');
 
-    val header = thm_header i ([pos, Position.thread_data ()]) name prop1 NONE;
+    val header =
+      thm_header i ([pos, Position.thread_data ()]) (Context.theory_long_name thy) name prop1 NONE;
     val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
     val head = PThm (header, thm_body);
     val proof =

--- a/src/Pure/term.scala	Thu Aug 15 16:38:55 2019 +0200
+++ b/src/Pure/term.scala	Thu Aug 15 16:57:09 2019 +0200
@@ -58,7 +58,8 @@
   case class PAxm(name: String, types: List[Typ]) extends Proof
   case class OfClass(typ: Typ, cls: String) extends Proof
   case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
-  case class PThm(serial: Long, pseudo_name: String, types: List[Typ]) extends Proof
+  case class PThm(serial: Long, theory_name: String, pseudo_name: String, types: List[Typ])
+    extends Proof
 
 
   /* Pure logic */
@@ -184,8 +185,8 @@
               case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
               case Oracle(name, prop, types) =>
                 store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
-              case PThm(serial, name, types) =>
-                store(PThm(serial, cache_string(name), cache_typs(types)))
+              case PThm(serial, theory_name, name, types) =>
+                store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
             }
         }
       }

--- a/src/Pure/term_xml.scala	Thu Aug 15 16:38:55 2019 +0200
+++ b/src/Pure/term_xml.scala	Thu Aug 15 16:57:09 2019 +0200
@@ -66,6 +66,6 @@
         { case (List(a), b) => PAxm(a, list(typ)(b)) },
         { case (List(a), b) => OfClass(typ(b), a) },
         { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
-        { case (List(a, b), c) => PThm(long_atom(a), b, list(typ)(c)) }))
+        { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
   }
 }