# HG changeset patch
# User wenzelm
# Date 1571325853 -7200
# Node ID aadb5c23af24d9b70e552082f4d851877d14ddb3
# Parent  f21a76a4d01f8c15718b5f798a817684c9038201
clarified proof_boxes (requires prune_proofs=false);

diff -r f21a76a4d01f -r aadb5c23af24 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Thu Oct 17 16:10:44 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Thu Oct 17 17:24:13 2019 +0200
@@ -253,6 +253,8 @@
       #> Thm.check_hyps (Context.Theory thy)
       #> Thm.strip_shyps;
 
+    val lookup_thm_id = Global_Theory.lookup_thm_id thy;
+
     fun entity_markup_thm (serial, (name, i)) =
       let
         val space = Facts.space_of (Global_Theory.facts_of thy);
@@ -260,19 +262,17 @@
         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;
 
-    fun encode_thm raw_thm =
+    fun encode_thm serial raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
+        fun defined (thm_id: Proofterm.thm_id) =
+          if #serial thm_id = serial then false else is_some (lookup_thm_id thm_id);
+
         val thm = clean_thm raw_thm;
-        val thm_name = Thm.derivation_name thm;
-        val raw_proof =
-          if Proofterm.export_enabled () then
-            Thm.reconstruct_proof_of thm
-            |> thm_name <> "" ? Proofterm.expand_proof thy [(thm_name, NONE)]
-          else Proofterm.MinProof;
         val (prop, SOME proof) =
-          standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME raw_proof);
-        val proof_boxes = Proofterm.proof_boxes proof;
+          SOME (if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof)
+          |> standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
+        val proof_boxes = Proofterm.proof_boxes defined proof;
       in
         (prop, (deps, (proof, proof_boxes))) |>
           let
@@ -285,7 +285,7 @@
     fun buffer_export_thm (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));
+        val body = encode_thm serial (Global_Theory.get_thm_name thy (thm_name, Position.none));
       in YXML.buffer (XML.Elem (markup, body)) end;
 
     val _ =
diff -r f21a76a4d01f -r aadb5c23af24 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Oct 17 16:10:44 2019 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 17 17:24:13 2019 +0200
@@ -181,7 +181,7 @@
   type thm_id = {serial: serial, theory_name: string}
   val thm_id: thm -> thm_id
   val get_id: sort list -> term list -> term -> proof -> thm_id option
-  val proof_boxes: proof -> thm_id list
+  val proof_boxes: (thm_id -> bool) -> proof -> thm_id list
 end
 
 structure Proofterm : PROOFTERM =
@@ -2255,7 +2255,7 @@
 end;
 
 
-(* get PThm identity *)
+(* PThm identity *)
 
 fun get_identity shyps hyps prop prf =
   let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
@@ -2270,37 +2270,41 @@
   Option.map #name (get_identity shyps hyps prop prf) |> the_default "";
 
 
+(* thm_id *)
+
 type thm_id = {serial: serial, theory_name: string};
 
+fun make_thm_id (serial, theory_name) : thm_id =
+  {serial = serial, theory_name = theory_name};
+
 fun thm_id (serial, thm_node) : thm_id =
-  {serial = serial, theory_name = thm_node_theory_name thm_node};
+  make_thm_id (serial, thm_node_theory_name thm_node);
 
 fun get_id shyps hyps prop prf : thm_id option =
   (case get_identity shyps hyps prop prf of
     NONE => NONE
   | SOME {name = "", ...} => NONE
-  | SOME {serial, theory_name, ...} => SOME {serial = serial, theory_name = theory_name});
+  | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name)));
 
 
-(* proof boxes *)
+(* proof boxes: undefined PThm nodes *)
 
-fun proof_boxes proof =
+fun proof_boxes defined proof =
   let
-    fun boxes_of (AbsP (_, _, prf)) = boxes_of prf
-      | boxes_of (Abst (_, _, prf)) = boxes_of prf
-      | boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2
+    fun boxes_of (Abst (_, _, prf)) = boxes_of prf
+      | boxes_of (AbsP (_, _, prf)) = boxes_of prf
       | boxes_of (prf % _) = boxes_of prf
-      | boxes_of (PThm ({serial = i, name = "", theory_name, ...}, thm_body)) =
+      | boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2
+      | boxes_of (PThm ({serial = i, theory_name = thy, ...}, thm_body)) =
           (fn boxes =>
-            if Inttab.defined boxes i then boxes
+            if defined (make_thm_id (i, thy)) orelse Inttab.defined boxes i then boxes
             else
               let
-                val prf = thm_body_proof_raw thm_body;
-                val boxes' = Inttab.update (i, theory_name) boxes;
-              in boxes_of prf boxes' end)
+                val prf' = thm_body_proof_raw thm_body;
+                val boxes' = Inttab.update (i, thy) boxes;
+              in boxes_of prf' boxes' end)
       | boxes_of _ = I;
-    val boxes = boxes_of proof Inttab.empty;
-  in Inttab.fold_rev (fn (i, thy) => cons {serial = i, theory_name = thy}) boxes [] end;
+  in Inttab.fold_rev (cons o make_thm_id) (boxes_of proof Inttab.empty) [] end;
 
 end;