diff -r c85efa2be619 -r d32ed8927a42 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/more_thm.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -682,9 +682,13 @@
   (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths);
 
 fun consolidate_theory thy =
-  rev (Proofs.get thy)
-  |> maps (map (Thm.transfer thy) o Lazy.force)
-  |> Thm.consolidate;
+  let
+    val thms =
+      rev (Proofs.get thy)
+      |> maps (map (Thm.transfer thy) o Lazy.force);
+    val _ = Thm.consolidate thms;
+    val _ = Thm.expose_proofs thy thms;
+  in () end;