src/Pure/Isar/outer_syntax.ML

--- a/src/Pure/Isar/outer_syntax.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu May 11 21:32:22 2023 +0200
@@ -325,7 +325,8 @@
   command ("ML", \<^here>) "ML text within theory or local theory"
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () =>
+        (Local_Theory.touch_ml_env #>
+          ML_Context.exec (fn () =>
             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
           Local_Theory.propagate_ml_env)));