# HG changeset patch
# User wenzelm
# Date 1635501542 -7200
# Node ID d622d1dce05cbc35d1c6e4dc265c22609d45990d
# Parent  e495ab64c6949e14aec203b642b6705d516b7125
avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);

diff -r e495ab64c694 -r d622d1dce05c src/Pure/ML/ml_instantiate.ML
--- a/src/Pure/ML/ml_instantiate.ML	Fri Oct 29 11:57:49 2021 +0200
+++ b/src/Pure/ML/ml_instantiate.ML	Fri Oct 29 11:59:02 2021 +0200
@@ -74,7 +74,7 @@
 fun put_thms ths ctxt =
   let
     val (i, thms) = Data.get ctxt;
-    val ctxt' = ctxt |> Data.put (i + 1, Inttab.update (i, ths) thms);
+    val ctxt' = ctxt |> Data.put (i + 1, Inttab.update (i, map Thm.trim_context ths) thms);
   in (i, ctxt') end;
 
 fun get_thms ctxt i = the (Inttab.lookup (#2 (Data.get ctxt)) i);