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)