# HG changeset patch
# User wenzelm
# Date 1571494179 -7200
# Node ID 9e05f382e749f60cf48547a06b6a408b47bd6bf1
# Parent  3828a57e537d5578a651d65b90075aab0cf5d273
export toplevel proof similar to named PThm;

diff -r 3828a57e537d -r 9e05f382e749 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Oct 19 15:32:32 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sat Oct 19 16:09:39 2019 +0200
@@ -262,15 +262,15 @@
     fun encode_thm thm_id raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
+        val thm = Thm.unconstrainT (clean_thm raw_thm);
         val dep_boxes =
-          raw_thm |> Thm_Deps.proof_boxes (fn thm_id' =>
+          thm |> Thm_Deps.proof_boxes (fn thm_id' =>
             if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id'));
         val boxes = dep_boxes @ [thm_id];
-
-        val thm = clean_thm raw_thm;
         val (prop, SOME 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 _ = Proofterm.commit_proof proof;
       in
         (prop, (deps, (boxes, proof))) |>
           let
diff -r 3828a57e537d -r 9e05f382e749 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Oct 19 15:32:32 2019 +0200
+++ b/src/Pure/proofterm.ML	Sat Oct 19 16:09:39 2019 +0200
@@ -171,6 +171,7 @@
 
   val export_enabled: unit -> bool
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
+  val commit_proof: proof -> unit
   val thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> string * Position.T -> sort list ->
     term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof
@@ -2117,6 +2118,24 @@
 
 fun export_enabled () = Options.default_bool "export_proofs";
 
+fun commit_proof proof =
+  let
+    fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
+      | export_boxes (Abst (_, _, prf)) = export_boxes prf
+      | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2
+      | export_boxes (prf % _) = export_boxes prf
+      | export_boxes (PThm ({serial = i, name = "", ...}, thm_body)) =
+          (fn boxes =>
+            if Inttab.defined boxes i then boxes
+            else
+              let
+                val prf = thm_body_proof_raw thm_body;
+                val boxes' = Inttab.update (i, thm_body_export_proof thm_body) boxes;
+              in export_boxes prf boxes' end)
+      | export_boxes _ = I;
+    val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
+  in List.app (Lazy.force o #2) boxes end;
+
 local
 
 fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) =
@@ -2162,28 +2181,10 @@
       strict = false}
   end;
 
-fun force_export_boxes proof =
-  let
-    fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
-      | export_boxes (Abst (_, _, prf)) = export_boxes prf
-      | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2
-      | export_boxes (prf % _) = export_boxes prf
-      | export_boxes (PThm ({serial = i, name = "", ...}, thm_body)) =
-          (fn boxes =>
-            if Inttab.defined boxes i then boxes
-            else
-              let
-                val prf = thm_body_proof_raw thm_body;
-                val boxes' = Inttab.update (i, thm_body_export_proof thm_body) boxes;
-              in export_boxes prf boxes' end)
-      | export_boxes _ = I;
-    val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
-  in List.app (Lazy.force o #2) boxes end;
-
 fun export thy i prop prf =
   if export_enabled () then
     let
-      val _ = force_export_boxes prf;
+      val _ = commit_proof prf;
       val _ = export_proof thy i prop prf;
     in () end
   else ();