# HG changeset patch
# User wenzelm
# Date 1243862759 -7200
# Node ID 3ffa005c7701f0296cbe2c6351d2dff8500bb1b2
# Parent  89f218fcab2a53595fb30ec7296b311bec20a2d9
removed print function from global ML name space, to reduce risk of surprises;

diff -r 89f218fcab2a -r 3ffa005c7701 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Mon Jun 01 13:32:54 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Mon Jun 01 15:25:59 2009 +0200
@@ -17,6 +17,8 @@
 
 val forget_structure = PolyML.Compiler.forgetStructure;
 
+val _ = PolyML.Compiler.forgetValue "print";
+
 
 (* Compiler options *)