# HG changeset patch
# User wenzelm
# Date 1458206503 -3600
# Node ID cdd6db02eae85724b0299fe74aeee243e060bed9
# Parent  dfd6fe970503c470fc39d3e671d7d1e93f24859b
tuned signature;

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);
diff -r dfd6fe970503 -r cdd6db02eae8 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Thu Mar 17 10:00:38 2016 +0100
+++ b/src/Pure/ML/ml_name_space.ML	Thu Mar 17 10:21:43 2016 +0100
@@ -10,16 +10,17 @@
 
   type T = PolyML.NameSpace.nameSpace;
   val global = PolyML.globalNameSpace;
-  val forget_global_structure = PolyML.Compiler.forgetStructure;
 
   type valueVal = Values.value;
   fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
   val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
+  val forget_val = PolyML.Compiler.forgetValue;
 
   type typeVal = TypeConstrs.typeConstr;
   fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
   val initial_type = #allType global ();
+  val forget_type = PolyML.Compiler.forgetType;
 
   type fixityVal = Infixes.fixity;
   fun displayFix (_: string, x) = Infixes.print x;
@@ -28,6 +29,7 @@
   type structureVal = Structures.structureVal;
   fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
   val initial_structure = #allStruct global ();
+  val forget_structure = PolyML.Compiler.forgetStructure;
 
   type signatureVal = Signatures.signatureVal;
   fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
diff -r dfd6fe970503 -r cdd6db02eae8 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Mar 17 10:00:38 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 17 10:21:43 2016 +0100
@@ -28,20 +28,20 @@
 use "Concurrent/multithreading.ML";
 
 use "Concurrent/unsynchronized.ML";
-val _ = PolyML.Compiler.forgetValue "ref";
-val _ = PolyML.Compiler.forgetType "ref";
+val _ = ML_Name_Space.forget_val "ref";
+val _ = ML_Name_Space.forget_type "ref";
 
 
 (* pervasive environment *)
 
-val _ = PolyML.Compiler.forgetValue "isSome";
-val _ = PolyML.Compiler.forgetValue "getOpt";
-val _ = PolyML.Compiler.forgetValue "valOf";
-val _ = PolyML.Compiler.forgetValue "foldl";
-val _ = PolyML.Compiler.forgetValue "foldr";
-val _ = PolyML.Compiler.forgetValue "print";
-val _ = PolyML.Compiler.forgetValue "explode";
-val _ = PolyML.Compiler.forgetValue "concat";
+val _ = ML_Name_Space.forget_val "isSome";
+val _ = ML_Name_Space.forget_val "getOpt";
+val _ = ML_Name_Space.forget_val "valOf";
+val _ = ML_Name_Space.forget_val "foldl";
+val _ = ML_Name_Space.forget_val "foldr";
+val _ = ML_Name_Space.forget_val "print";
+val _ = ML_Name_Space.forget_val "explode";
+val _ = ML_Name_Space.forget_val "concat";
 
 val ord = SML90.ord;
 val chr = SML90.chr;