diff -r dfd6fe970503 -r cdd6db02eae8 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Thu Mar 17 10:00:38 2016 +0100
+++ b/src/Pure/ML/ml_env.ML	Thu Mar 17 10:21:43 2016 +0100
@@ -77,7 +77,7 @@
 fun forget_structure name =
   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
     let
-      val _ = if bootstrap then ML_Name_Space.forget_global_structure name else ();
+      val _ = if bootstrap then ML_Name_Space.forget_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, breakpoints) end);