Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);
authorwenzelm
Fri, 29 Oct 2021 11:59:02 +0200
changeset 74620 d622d1dce05c
parent 74619 e495ab64c694
child 74621 82ff15b980e9
avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);
src/Pure/ML/ml_instantiate.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle