diff -r 2187de552bd4 -r 2c6f355e52bb src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Dec 26 20:33:38 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 26 22:14:44 2023 +0100
@@ -2090,7 +2090,9 @@
     val ((i, (_, zproof1)), zproof2) = ZTerm.thm_proof thy name hyps prop zproof;
     val der1 = if Options.default_bool "prune_proofs" then deriv [] ZDummy else deriv zboxes zproof1;
     val der2 = deriv [] zproof2;
-    val thy' = thy |> (map_zproofs o Inttab.update) (i, {name = name, thm = Thm (der1, args)});
+
+    val thm' = trim_context (Thm (der1, args));
+    val thy' = thy |> (map_zproofs o Inttab.update) (i, {name = name, thm = thm'});
   in (Thm (der2, args), thy') end;