src/Pure/ML/ml_context.ML
changeset 78035 bd5f6cee8001
parent 76884 a004c5322ea4
child 78689 37b49c592265
--- a/src/Pure/ML/ml_context.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu May 11 21:32:22 2023 +0200
@@ -228,7 +228,9 @@
     SOME context' => context'
   | NONE => error "Missing context after execution");
 
-fun expression pos ants = exec (fn () => eval ML_Compiler.flags pos ants);
+fun expression pos ants =
+  Local_Theory.touch_ml_env #>
+  exec (fn () => eval ML_Compiler.flags pos ants);
 
 end;