src/HOL/Import/proof_kernel.ML

           | G 4 f ctxt x = G 3 f (Config.put show_brackets true ctxt) x
           | G _ _ _ _ = raise SMART_STRING
         fun F n =
             let
                 val str = G n Syntax.string_of_term ctxt tn
-                val _ = warning (PolyML.makestring (n, str))
+                val _ = warning (@{make_string} (n, str))
                 val u = Syntax.parse_term ctxt str
                 val u = if t = t' then u else HOLogic.mk_Trueprop u
                 val u = Syntax.check_term ctxt (Type.constraint T u)
             in
                 if match u