--- a/src/Pure/ML/ml_env.ML Wed Dec 10 17:55:31 2014 +0100
+++ b/src/Pure/ML/ml_env.ML Wed Dec 10 19:24:54 2014 +0100
@@ -8,6 +8,7 @@
signature ML_ENV =
sig
val inherit: Context.generic -> Context.generic -> Context.generic
+ val forget_structure: string -> Context.generic -> Context.generic
val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
val local_context: use_context
val local_name_space: ML_Name_Space.T
@@ -63,6 +64,14 @@
val inherit = Env.put o Env.get;
+fun forget_structure name =
+ Env.map (fn {bootstrap, tables, sml_tables} =>
+ let
+ val _ = if bootstrap then ML_Name_Space.forget_global_structure name else ();
+ val tables' =
+ (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables);
+ in make_data (bootstrap, tables', sml_tables) end);
+
(* name space *)