diff -r 10162c01bd78 -r b06db8e4476b src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Mon Jun 12 00:36:52 2006 +0200
+++ b/src/Pure/Tools/invoke.ML	Mon Jun 12 09:14:41 2006 +0200
@@ -77,7 +77,7 @@
             |> Element.map_ctxt_values I I (ProofContext.export ctxt'' ctxt);
               (* FIXME export typs/terms *)
 
-          val _ = PolyML.print notes;
+          val _ = print notes;
 
           val notes' = notes
             |> Attrib.map_facts (Attrib.attribute_i thy)