trim context of persistent data;
authorwenzelm
Fri Feb 16 19:30:28 2018 +0100 (17 months ago)
changeset 6763025cb2299f8a4
parent 67629 357737ccb138
child 67631 b7d90c4a3897
trim context of persistent data;
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Feb 16 18:55:42 2018 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Feb 16 19:30:28 2018 +0100
     1.3 @@ -349,10 +349,12 @@
     1.4      val thms = Simplifier.mksimps (Proof_Context.init_global thy) thm;
     1.5    in
     1.6      thy
     1.7 -    |> Computation_Preproc_Data.map (union Thm.eq_thm_prop thms)
     1.8 +    |> Computation_Preproc_Data.map (fold (insert Thm.eq_thm_prop o Thm.trim_context) thms)
     1.9    end;
    1.10  
    1.11 -fun get ctxt = Computation_Preproc_Data.get (Proof_Context.theory_of ctxt);
    1.12 +fun get ctxt =
    1.13 +  Computation_Preproc_Data.get (Proof_Context.theory_of ctxt)
    1.14 +  |> map (Thm.transfer (Proof_Context.theory_of ctxt))
    1.15  
    1.16  in
    1.17