--- 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);
--- 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);
--- 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;