# HG changeset patch # User wenzelm # Date 1254235322 -7200 # Node ID bf8881f6e3431d2f6a151cacb441f5d59bed6cc8 # Parent 9dd0a2f8342953d7182d5193f437301ab775467d hide "ref" by default, to enforce excplicit indication as Unsynchronized; diff -r 9dd0a2f83429 -r bf8881f6e343 src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Tue Sep 29 16:24:36 2009 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Tue Sep 29 16:42:02 2009 +0200 @@ -20,6 +20,8 @@ val forget_structure = PolyML.Compiler.forgetStructure; val _ = PolyML.Compiler.forgetValue "print"; +val _ = PolyML.Compiler.forgetValue "ref"; +val _ = PolyML.Compiler.forgetType "ref"; (* Compiler options *)