diff -r b05d78bfc67c -r c85efa2be619 src/Pure/Isar/class_declaration.ML
--- 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;