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.
trim context of persistent data;
authorwenzelm
Fri, 16 Feb 2018 19:30:28 +0100
changeset 67630 25cb2299f8a4
parent 67629 357737ccb138
child 67631 b7d90c4a3897
trim context of persistent data;
src/Tools/Code/code_runtime.ML file | annotate | diff | comparison | revisions 
--- a/src/Tools/Code/code_runtime.ML	Fri Feb 16 18:55:42 2018 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Feb 16 19:30:28 2018 +0100
@@ -349,10 +349,12 @@
     val thms = Simplifier.mksimps (Proof_Context.init_global thy) thm;
   in
     thy
-    |> Computation_Preproc_Data.map (union Thm.eq_thm_prop thms)
+    |> Computation_Preproc_Data.map (fold (insert Thm.eq_thm_prop o Thm.trim_context) thms)
   end;
 
-fun get ctxt = Computation_Preproc_Data.get (Proof_Context.theory_of ctxt);
+fun get ctxt =
+  Computation_Preproc_Data.get (Proof_Context.theory_of ctxt)
+  |> map (Thm.transfer (Proof_Context.theory_of ctxt))
 
 in
isabelle