src/Pure/proofterm.ML

 signature BASIC_PROOFTERM =
 sig
   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
    | PBound of int
    | Abst of string * typ option * proof

   val proofs: int Unsynchronized.ref
   type pthm = proof_serial * thm_node
   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
   val thm_node_name: thm_node -> string
   val thm_node_prop: thm_node -> term

 (** datatype proof **)
 
 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
  | PBound of int
  | Abst of string * typ option * proof

 val join_proof = Future.join #> proof_of;
 
 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 ();
 
 fun thm_body body =
   Thm_Body {export_proof = no_export_proof, open_proof = I, body = Future.value body};

   fn a %% b => ([], pair proof proof (a, b)),
   fn Hyp a => ([], term a),
   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}) =
   triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
 and pthm (a, thm_node) =

   fn a %% b => ([], pair full_proof full_proof (a, b)),
   fn Hyp a => ([], term a),
   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
 
 val encode = proof;
 val encode_body = proof_body;

   fn ([], a) => op %% (pair proof proof a),
   fn ([], a) => Hyp (term a),
   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
 and pthm x =
   let val (a, (b, c, d)) = pair int (triple string term proof_body) x

           (proof prf1 %% Same.commit proof prf2
             handle Same.SAME => prf1 %% proof prf2)
       | 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;
 
 fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c));
 fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;

   | size_of_proof _ = 1;
 
 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;
 
 
 (* utilities *)
 

           PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
       | norm (OfClass (T, c)) =
           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;
 
 
 (* remove some types in proof term (to save space) *)

           PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
       | lift' _ _ (OfClass (T, c)) =
           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);
 
     val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
     val k = length ps;

             NONE => raise Same.SAME
           | SOME prf' => incr_pboundvars plev tlev prf')
       | 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;
 
 (*A fast unification filter: true unless the two terms cannot be unified.
   Terms must be NORMAL.  Treats all Vars as distinct. *)

       if named orelse not (export_enabled ()) then no_export_proof
       else Lazy.lazy (fn () => join_proof body' |> open_proof |> export_proof thy i prop1);
 
     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 =
       if unconstrain then
         proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)