src/Pure/more_thm.ML

   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
   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
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit

 
 
 
 (** 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);
 
 fun standard_proof_of {full, expand_name} thm =
   let val thy = Thm.theory_of_thm thm in