more robust expose_proofs corresponding to register_proofs/consolidate_theory;
expose_proofs of class algebra more aggresively, to ensure early export within original theory/session context;

--- a/src/Pure/Isar/class_declaration.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -84,7 +84,6 @@
       in
         Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'')
           (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm'']))
-        |> tap (Thm.expose_proof thy)
       end;
     val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
 
@@ -103,9 +102,7 @@
       REPEAT (SOMEGOAL
         (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
           ORELSE' assume_tac ctxt));
-    val of_class =
-      Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context)
-      |> tap (Thm.expose_proof thy);
+    val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
   in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
 
 

--- a/src/Pure/Isar/element.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/Isar/element.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -275,7 +275,7 @@
   Witness (t,
     Goal.prove ctxt [] [] (mark_witness t)
       (fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac)
-    |> Thm.expose_derivation \<^here>);
+    |> Thm.close_derivation \<^here>);
 
 
 local
@@ -290,7 +290,7 @@
       (map o map) (fn prop => (mark_witness prop, [])) wit_propss @
         [map (rpair []) eq_props];
     fun after_qed' thmss =
-      let val (wits, eqs) = split_last ((map o map) (Thm.expose_derivation \<^here>) thmss);
+      let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here>) thmss);
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness end;
 
@@ -324,7 +324,7 @@
 fun conclude_witness ctxt (Witness (_, th)) =
   Goal.conclude th
   |> Raw_Simplifier.norm_hhf_protect ctxt
-  |> Thm.expose_derivation \<^here>;
+  |> Thm.close_derivation \<^here>;
 
 fun pretty_witness ctxt witn =
   let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in

--- a/src/Pure/Isar/expression.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -720,8 +720,7 @@
         compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
         compose_tac defs_ctxt
           (false,
-            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1)
-      |> tap (Thm.expose_proof defs_thy);
+            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF

--- a/src/Pure/Thy/export_theory.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -275,9 +275,7 @@
           else MinProof;
         val (prop, SOME proof) =
           standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0);
-        val _ =
-          if Proofterm.export_proof_boxes_required thy
-          then Proofterm.export_proof_boxes [proof] else ();
+        val _ = Thm.expose_proofs thy [thm];
       in
         (prop, deps, proof) |>
           let

--- a/src/Pure/global_theory.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/global_theory.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -288,11 +288,7 @@
     fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy);
 
 fun apply_facts name_flags1 name_flags2 (b, facts) thy =
-  if Binding.is_empty b then
-    let
-      val (thms, thy') = app_facts facts thy;
-      val _ = Thm.expose_proofs thy' thms;
-    in register_proofs thms thy' end
+  if Binding.is_empty b then app_facts facts thy |-> register_proofs
   else
     let
       val name_pos = bind_name thy b;

--- a/src/Pure/more_thm.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/more_thm.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -682,9 +682,13 @@
   (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths);
 
 fun consolidate_theory thy =
-  rev (Proofs.get thy)
-  |> maps (map (Thm.transfer thy) o Lazy.force)
-  |> Thm.consolidate;
+  let
+    val thms =
+      rev (Proofs.get thy)
+      |> maps (map (Thm.transfer thy) o Lazy.force);
+    val _ = Thm.consolidate thms;
+    val _ = Thm.expose_proofs thy thms;
+  in () end;
 
 
 

--- a/src/Pure/proofterm.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/proofterm.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -46,7 +46,6 @@
   val thm_node_body: thm_node -> proof_body future
   val thm_node_thms: thm_node -> thm list
   val join_thms: thm list -> proof_body list
-  val consolidate: proof_body list -> unit
   val make_thm: thm_header -> thm_body -> thm
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms:
@@ -176,7 +175,7 @@
   val export_enabled: unit -> bool
   val export_standard_enabled: unit -> bool
   val export_proof_boxes_required: theory -> bool
-  val export_proof_boxes: proof list -> unit
+  val export_proof_boxes: proof_body list -> unit
   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 ->
@@ -223,10 +222,10 @@
    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}
+  Thm_Body of {open_proof: proof -> proof, body: proof_body future}
 and thm_node =
   Thm_Node of {theory_name: string, name: string, prop: term,
-    body: proof_body future, consolidate: unit lazy};
+    body: proof_body future, export: unit lazy, consolidate: unit lazy};
 
 type oracle = string * term option;
 val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
@@ -246,11 +245,7 @@
 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};
-fun thm_body_export_proof (Thm_Body {export_proof, ...}) = export_proof;
+fun thm_body body = Thm_Body {open_proof = I, body = Future.value body};
 fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body;
 fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body);
 
@@ -260,24 +255,33 @@
 val thm_node_prop = #prop o rep_thm_node;
 val thm_node_body = #body o rep_thm_node;
 val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms);
+val thm_node_export = #export o rep_thm_node;
 val thm_node_consolidate = #consolidate o rep_thm_node;
 
 fun join_thms (thms: thm list) =
   Future.joins (map (thm_node_body o #2) thms);
 
-val consolidate =
+val consolidate_bodies =
   maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
   #> Lazy.consolidate #> map Lazy.force #> ignore;
 
-fun make_thm_node theory_name name prop body =
-  Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body,
-    consolidate =
+fun make_thm_node theory_name name prop body export =
+  let
+    val body' = body
+      |> Options.default_bool "prune_proofs" ? (Future.map o map_proof_of) (K MinProof);
+    val consolidate =
       Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
-        let val PBody {thms, ...} = Future.join body
-        in consolidate (join_thms thms) end)};
+        let val PBody {thms, ...} = Future.join body'
+        in consolidate_bodies (join_thms thms) end);
+  in
+    Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body',
+      export = export, consolidate = consolidate}
+  end;
+
+val no_export = Lazy.value ();
 
 fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
-  (serial, make_thm_node theory_name name prop body);
+  (serial, make_thm_node theory_name name prop body no_export);
 
 
 (* proof atoms *)
@@ -339,10 +343,10 @@
   | no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf)
   | no_body_proofs (prf % t) = no_body_proofs prf % t
   | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2
-  | no_body_proofs (PThm (header, Thm_Body {export_proof, open_proof, body})) =
+  | no_body_proofs (PThm (header, Thm_Body {open_proof, body})) =
       let
         val body' = Future.value (no_proof_body (join_proof body));
-        val thm_body' = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
+        val thm_body' = Thm_Body {open_proof = open_proof, body = body'};
       in PThm (header, thm_body') end
   | no_body_proofs a = a;
 
@@ -443,7 +447,7 @@
   let
     val (a, (b, (c, (d, e)))) =
       pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x
-  in (a, make_thm_node b c d (Future.value e)) end;
+  in (a, make_thm_node b c d (Future.value e) no_export) end;
 
 in
 
@@ -1959,7 +1963,7 @@
 
 fun fulfill_norm_proof thy ps body0 =
   let
-    val _ = consolidate (map #2 ps @ [body0]);
+    val _ = consolidate_bodies (map #2 ps @ [body0]);
     val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
     val oracles =
       unions_oracles
@@ -2097,24 +2101,19 @@
   Context.theory_name thy = Context.PureN orelse
     (export_enabled () andalso not (export_standard_enabled ()));
 
-fun export_proof_boxes proofs =
+fun export_proof_boxes bodies =
   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, ...}, thm_body)) =
-          (fn boxes =>
-            if Inttab.defined boxes i then boxes
-            else
-              let
-                val prf' = thm_body_proof_raw thm_body;
-                val export = thm_body_export_proof thm_body;
-                val boxes' = Inttab.update (i, export) boxes;
-              in export_boxes prf' boxes' end)
-      | export_boxes _ = I;
-    val boxes = (proofs, Inttab.empty) |-> fold export_boxes |> Inttab.dest;
-  in List.app (Lazy.force o #2) boxes end;
+    fun export_thm (i, thm_node) boxes =
+      if Inttab.defined boxes i then boxes
+      else
+        boxes
+        |> Inttab.update (i, thm_node_export thm_node)
+        |> fold export_thm (thm_node_thms thm_node);
+
+    fun export_body (PBody {thms, ...}) = fold export_thm thms;
+
+    val exports = (bodies, Inttab.empty) |-> fold export_body |> Inttab.dest;
+  in List.app (Lazy.force o #2) exports end;
 
 local
 
@@ -2160,18 +2159,6 @@
       strict = false} xml
   end;
 
-fun export thy i prop prf =
-  if export_enabled () then
-    let
-      val _ = export_proof_boxes [prf];
-      val _ = export_proof thy i prop prf;
-    in () end
-  else ();
-
-fun prune proof =
-  if Options.default_bool "prune_proofs" then MinProof
-  else proof;
-
 fun prepare_thm_proof unconstrain thy classrel_proof arity_proof
     (name, pos) shyps hyps concl promises body =
   let
@@ -2188,15 +2175,12 @@
         (PBody {oracles = oracles0, thms = thms0,
           proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof});
 
-    fun publish i = map_proof_of (rew_proof thy #> tap (export thy i prop1) #> prune);
-    val open_proof = not named ? rew_proof thy;
-
     fun new_prf () =
       let
         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;
+        val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
       in (i, fulfill_proof_future thy promises postproc body0) end;
 
     val (i, body') =
@@ -2207,25 +2191,27 @@
             let
               val Thm_Body {body = body', ...} = thm_body';
               val i = if a = "" andalso named then serial () else ser;
-            in (i, body' |> ser <> i ? Future.map (publish i)) end
+            in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
           else new_prf ()
       | _ => new_prf ());
 
-    val export_proof =
-      if named orelse not (export_enabled ()) then no_export_proof
-      else
+    val open_proof = not named ? rew_proof thy;
+
+    val export =
+      if export_enabled () then
         Lazy.lazy (fn () =>
           join_proof body' |> open_proof |> export_proof thy i prop1 handle exn =>
             if Exn.is_interrupt exn then
               raise Fail ("Interrupt: potential resource problems while exporting proof " ^
                 string_of_int i)
-            else Exn.reraise exn);
+            else Exn.reraise exn)
+      else no_export;
 
     val theory_name = Context.theory_long_name thy;
-    val thm = (i, make_thm_node theory_name name prop1 body');
+    val thm = (i, make_thm_node theory_name name prop1 body' export);
 
     val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE;
-    val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
+    val thm_body = Thm_Body {open_proof = open_proof, body = body'};
     val head = PThm (header, thm_body);
     val proof =
       if unconstrain then

--- a/src/Pure/thm.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/thm.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -113,7 +113,6 @@
   val expand_name: thm -> Proofterm.thm_header -> string option
   val name_derivation: string * Position.T -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
-  val expose_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
   val axiom: theory -> string -> thm
   val all_axioms_of: theory -> (string * thm) list
@@ -765,7 +764,7 @@
 
 fun expose_proofs thy thms =
   if Proofterm.export_proof_boxes_required thy then
-    Proofterm.export_proof_boxes (map (proof_of o transfer thy) thms)
+    Proofterm.export_proof_boxes (proof_bodies_of (map (transfer thy) thms))
   else ();
 
 fun expose_proof thy = expose_proofs thy o single;
@@ -1044,10 +1043,6 @@
     if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
     else name_derivation ("", pos) thm);
 
-fun expose_derivation pos thm =
-  close_derivation pos thm
-  |> tap (expose_proof (theory_of_thm thm));
-
 val trim_context = solve_constraints #> trim_context_thm;
 
 
@@ -2253,7 +2248,8 @@
               |> (map_classrels o Symreltab.update) ((c1, c2),
                 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
                 |> standard_tvars
-                |> expose_derivation \<^here>
+                |> close_derivation \<^here>
+                |> tap (expose_proof thy2)
                 |> trim_context));
 
         val proven = is_classrel thy1;
@@ -2286,7 +2282,8 @@
             val th1 =
               (th RS the_classrel thy (c, c1))
               |> standard_tvars
-              |> expose_derivation \<^here>
+              |> close_derivation \<^here>
+              |> tap (expose_proof thy)
               |> trim_context;
           in SOME ((t, Ss, c1), (th1, thy_name, ser)) end);
     val finished' = finished andalso null completions;