forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;

--- a/src/Pure/ML-Systems/polyml_common.ML	Mon Oct 26 20:41:26 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Mon Oct 26 20:42:08 2009 +0100
@@ -18,6 +18,9 @@
 
 val forget_structure = PolyML.Compiler.forgetStructure;
 
+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";