expose derivations more thoroughly, notably for locale/class reasoning;

--- a/src/Pure/Isar/class_declaration.ML	Sun Nov 03 19:43:59 2019 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Sun Nov 03 20:38:08 2019 +0100
@@ -84,6 +84,7 @@
       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));
 
@@ -102,8 +103,9 @@
       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);
-
+    val of_class =
+      Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context)
+      |> tap (Thm.expose_proof thy);
   in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
 
 

--- a/src/Pure/Isar/element.ML	Sun Nov 03 19:43:59 2019 +0100
+++ b/src/Pure/Isar/element.ML	Sun Nov 03 20:38:08 2019 +0100
@@ -273,9 +273,9 @@
 
 fun prove_witness ctxt t tac =
   Witness (t,
-    Thm.close_derivation \<^here>
-      (Goal.prove ctxt [] [] (mark_witness t)
-        (fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac)));
+    Goal.prove ctxt [] [] (mark_witness t)
+      (fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac)
+    |> Thm.expose_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.close_derivation \<^here>) thmss);
+      let val (wits, eqs) = split_last ((map o map) (Thm.expose_derivation \<^here>) thmss);
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness end;
 
@@ -322,7 +322,9 @@
 end;
 
 fun conclude_witness ctxt (Witness (_, th)) =
-  Thm.close_derivation \<^here> (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
+  Goal.conclude th
+  |> Raw_Simplifier.norm_hhf_protect ctxt
+  |> Thm.expose_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 19:43:59 2019 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Nov 03 20:38:08 2019 +0100
@@ -720,7 +720,8 @@
         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);
+            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1)
+      |> tap (Thm.expose_proof defs_thy);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF

--- a/src/Pure/thm.ML	Sun Nov 03 19:43:59 2019 +0100
+++ b/src/Pure/thm.ML	Sun Nov 03 20:38:08 2019 +0100
@@ -103,6 +103,7 @@
   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
@@ -112,6 +113,7 @@
   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
@@ -766,6 +768,8 @@
     Proofterm.export_proof_boxes (map (proof_of o transfer thy) thms)
   else ();
 
+fun expose_proof thy = expose_proofs thy o single;
+
 
 (* future rule *)
 
@@ -1040,6 +1044,10 @@
     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;
 
 
@@ -2245,7 +2253,7 @@
               |> (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;
@@ -2278,7 +2286,7 @@
             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;
@@ -2306,12 +2314,13 @@
 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;
@@ -2319,9 +2328,10 @@
 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])