# HG changeset patch
# User wenzelm
# Date 1256586128 -3600
# Node ID 1b550123f1335f707ec45f57e90f6222d9611beb
# Parent  f3c8acbff503a86f79cbf7f00cdc00c7ea13f350
forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;

diff -r f3c8acbff503 -r 1b550123f133 src/Pure/ML-Systems/polyml_common.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";