1.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Jul 18 23:35:50 2011 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Jul 18 23:48:28 2011 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4          fun F n =
     1.5              let
     1.6                  val str = G n Syntax.string_of_term ctxt tn
     1.7 -                val _ = warning (PolyML.makestring (n, str))
     1.8 +                val _ = warning (@{make_string} (n, str))
     1.9                  val u = Syntax.parse_term ctxt str
    1.10                  val u = if t = t' then u else HOLogic.mk_Trueprop u
    1.11                  val u = Syntax.check_term ctxt (Type.constraint T u)