--- 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);
--- 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 *)