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