merged
authorhaftmann
Wed, 30 Sep 2009 19:04:48 +0200
changeset 32783 e43d761a742d
parent 32778 a92a18253f1e (diff)
parent 32782 faf347097852 (current diff)
child 32784 1a5dde5079ac
child 32805 9b535493ac8d
merged
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Wed Sep 30 17:23:00 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Wed Sep 30 19:04:48 2009 +0200
@@ -27,6 +27,7 @@
 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
 
 use "ML-Systems/compiler_polyml-5.3.ML";
+PolyML.Compiler.reportUnreferencedIds := true;
 
 
 (* toplevel pretty printing *)