# HG changeset patch
# User krauss
# Date 1311025708 -7200
# Node ID 09576fe8ef0847be502031ff35eadc80a88119aa
# Parent  182caf5cf0b600b7d6e5701499af9e8e1be78f74
killed use of PolyML.makestring

diff -r 182caf5cf0b6 -r 09576fe8ef08 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon Jul 18 23:35:50 2011 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Mon Jul 18 23:48:28 2011 +0200
@@ -220,7 +220,7 @@
         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)