src/Pure/Tools/invoke.ML

             Element.Notes (maps (Element.facts_of thy) elems')
             |> Element.satisfy_ctxt prems''
             |> 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)
             |> map (fn ((a, atts), facts) => ((a, atts @ more_atts), facts));