src/Pure/ML-Systems/polyml_common.ML
changeset 33213 1b550123f133
parent 33060 e66b41782cb5
child 34136 3dcb46ae6185
--- 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";