changeset 44766 | 09576fe8ef08 |
parent 44638 | 2bd54d4b5f3d |
child 44789 | 6ca79a354c51 |
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)