# HG changeset patch
# User wenzelm
# Date 1254315643 -7200
# Node ID a92a18253f1e94228487feb5383d05ab9bdc5405
# Parent  8ae3a48c69d9f8295e2be04c11fd1fbf05a6d2d5
report unreferenced ids;

diff -r 8ae3a48c69d9 -r a92a18253f1e src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Wed Sep 30 11:45:42 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Wed Sep 30 15:00:43 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 *)