src/Pure/thm.ML

   val proof_bodies_of: thm list -> proof_body list
   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 expose_proof: theory -> thm -> unit
   val future: thm future -> cterm -> thm
   val thm_deps: thm -> Proofterm.thm Ord_List.T
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
   val derivation_id: thm -> Proofterm.thm_id option
   val raw_derivation_name: thm -> string
   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
   val get_tags: thm -> Properties.T
   val map_tags: (Properties.T -> Properties.T) -> thm -> thm

 fun expose_proofs thy thms =
   if Proofterm.export_proof_boxes_required thy then
     Proofterm.export_proof_boxes (map (proof_of o transfer thy) thms)
   else ();
 
+fun expose_proof thy = expose_proofs thy o single;
+
 
 (* future rule *)
 
 fun future_result i orig_cert orig_shyps orig_prop thm =
   let

 
 fun close_derivation pos =
   solve_constraints #> (fn thm =>
     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;
 
 
 

             (false,
               thy2
               |> (map_classrels o Symreltab.update) ((c1, c2),
                 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
                 |> standard_tvars
-                |> close_derivation \<^here>
+                |> expose_derivation \<^here>
                 |> trim_context));
 
         val proven = is_classrel thy1;
         val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
         val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];

         else
           let
             val th1 =
               (th RS the_classrel thy (c, c1))
               |> standard_tvars
-              |> close_derivation \<^here>
+              |> expose_derivation \<^here>
               |> trim_context;
           in SOME ((t, Ss, c1), (th1, thy_name, ser)) end);
     val finished' = finished andalso null completions;
     val arities' = fold Aritytab.update completions arities;
   in (finished', arities') end;

 (* primitive rules *)
 
 fun add_classrel raw_th thy =
   let
     val th = strip_shyps (transfer thy raw_th);
+    val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context;
     val prop = plain_prop_of th;
     val (c1, c2) = Logic.dest_classrel prop;
   in
     thy
     |> Sign.primitive_classrel (c1, c2)
-    |> map_classrels (Symreltab.update ((c1, c2), th |> unconstrainT |> trim_context))
+    |> map_classrels (Symreltab.update ((c1, c2), th'))
     |> perhaps complete_classrels
     |> perhaps complete_arities
   end;
 
 fun add_arity raw_th thy =
   let
     val th = strip_shyps (transfer thy raw_th);
+    val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context;
     val prop = plain_prop_of th;
     val (t, Ss, c) = Logic.dest_arity prop;
-    val ar = ((t, Ss, c), (th |> unconstrainT |> trim_context, Context.theory_name thy, serial ()));
+    val ar = ((t, Ss, c), (th', Context.theory_name thy, serial ()));
   in
     thy
     |> Sign.primitive_arity (t, Ss, [c])
     |> map_arities (Aritytab.update ar #> curry (insert_arity_completions thy ar) true #> #2)
   end;