diff -r 357737ccb138 -r 25cb2299f8a4 src/Tools/Code/code_runtime.ML
--- 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