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;