diff -r 37085099e415 -r bd5f6cee8001 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/ML/ml_env.ML	Thu May 11 21:32:22 2023 +0200
@@ -26,6 +26,7 @@
   val Isabelle_operations: operations
   val SML_operations: operations
   val operations: Context.generic option -> string -> operations
+  val touch: Context.generic -> Context.generic
   val forget_structure: string -> Context.generic -> Context.generic
   val bootstrap_name_space: Context.generic -> Context.generic
   val add_name_space: string -> ML_Name_Space.T -> Context.generic -> Context.generic
@@ -127,6 +128,8 @@
 val get_env = Name_Space.get o #1 o Data.get;
 val get_tables = #1 oo get_env;
 
+val touch = Data.map I;
+
 fun update_tables env_name f context = context |> (Data.map o apfst) (fn envs =>
   let val _ = Name_Space.get envs env_name;
   in Name_Space.map_table_entry env_name (apfst f) envs end);