src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Thu Aug 13 11:05:19 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Thu Aug 13 11:40:31 2015 +0200
@@ -941,7 +941,7 @@
 fun biggest_hyp_first_tac i = fn st =>
   let
     val results = TERMFUN biggest_hypothesis (SOME i) st
-val _ = tracing ("result=" ^ PolyML.makestring results)
+val _ = tracing ("result=" ^ @{make_string} results)
   in
     if null results then no_tac st
     else