# HG changeset patch
# User wenzelm
# Date 1572792539 -3600
# Node ID 2c96e48027ebd0fa18ded1e7626ffec4fc73d230
# Parent  be689b7d81fdc45b49a42850a1cd52ca52aedb90
clarified modules;

diff -r be689b7d81fd -r 2c96e48027eb src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Nov 03 15:45:46 2019 +0100
+++ b/src/Pure/more_thm.ML	Sun Nov 03 15:48:59 2019 +0100
@@ -113,7 +113,6 @@
   val tag: string * string -> attribute
   val untag: string -> attribute
   val kind: string -> attribute
-  val expose_proofs: theory -> thm list -> unit
   val reconstruct_proof_of: thm -> Proofterm.proof
   val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
     thm -> Proofterm.proof
@@ -655,11 +654,6 @@
 
 (** proof terms **)
 
-fun expose_proofs thy thms =
-  if Proofterm.export_proof_boxes_required thy then
-    Proofterm.export_proof_boxes (map Thm.proof_of thms)
-  else ();
-
 fun reconstruct_proof_of thm =
   Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
 
diff -r be689b7d81fd -r 2c96e48027eb src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Nov 03 15:45:46 2019 +0100
+++ b/src/Pure/thm.ML	Sun Nov 03 15:48:59 2019 +0100
@@ -102,6 +102,7 @@
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
   val consolidate: thm list -> unit
+  val expose_proofs: theory -> thm list -> unit
   val future: thm future -> cterm -> thm
   val thm_deps: thm -> Proofterm.thm Ord_List.T
   val derivation_closed: thm -> bool
@@ -760,6 +761,11 @@
 
 val consolidate = ignore o proof_bodies_of;
 
+fun expose_proofs thy thms =
+  if Proofterm.export_proof_boxes_required thy then
+    Proofterm.export_proof_boxes (map proof_of thms)
+  else ();
+
 
 (* future rule *)