src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy

         [Pretty.str (n ^ " "),
          Syntax.pretty_term ctxt (#fmla data),
          Pretty.str (
           if is_none (#source_inf_opt data) then ""
           else ("\n\tannotation: " ^
-           PolyML.makestring (the (#source_inf_opt data : TPTP_Proof.source_info option))))])
+           @{make_string} (the (#source_inf_opt data : TPTP_Proof.source_info option))))])
     ) (rev fms);
 
 (*FIXME hack for testing*)
 fun test_fmla thy =
   TPTP_Reconstruct.get_fmlas_of_prob thy (hd prob_names);

   end
 
 val step_range_tester_tracing =
   step_range_tester
    (fn x => tracing ("@step " ^ Int.toString x))
-   (fn e => tracing ("!!" ^ PolyML.makestring e))
+   (fn e => tracing ("!!" ^ @{make_string} e))
 *}
 
 ML {*
 (*try to reconstruct each inference step*)
 if test_all @{context} orelse prob_names = []

             EVERY [tac1, tac2]
             THEN interleave_tacs tacs1 tacs2
       val thms_to_traceprint =
         map (fn thm => fn st =>
               (*FIXME uses makestring*)
-              print_tac ctxt (PolyML.makestring thm) st)
+              print_tac ctxt (@{make_string} thm) st)
 
     in
       if verbose then
         ListPair.unzip thm_tacs
         |> apfst (fn thms => enumerate 1 thms)

 else
   the_tactics
   |> hd
   |> map #1
   |> TPTP_Reconstruct_Library.enumerate 0
-  |> List.app (PolyML.makestring #> writeln)
+  |> List.app (@{make_string} #> writeln)
   *}
 
 ML {*
 fun leo2_tac_wrap ctxt prob_name step i st =
   rtac (interpret_leo2_inference ctxt prob_name step) i st

       if is_some thy' then
         SOME (TPTP_Reconstruct.naive_reconstruct_tacs (* metis_based_reconstruction_tac *)
 interpret_leo2_inference (* auto_based_reconstruction_tac *) (* oracle_based_reconstruction_tac *) prob_name (the ctxt'))
       else NONE
 
-(* val _ = tracing ("tt=" ^ PolyML.makestring the_tactics) *)
+(* val _ = tracing ("tt=" ^ @{make_string} the_tactics) *)
 
     val skeleton =
       if is_some thy' then
         SOME (TPTP_Reconstruct.make_skeleton (the ctxt')
               (TPTP_Reconstruct.get_pannot_of_prob (the thy') prob_name))

       val timer = Timer.startRealTimer ()
     in
       TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
        (test_partial_reconstruction thy
         #> light_output ? erase_inference_fmlas
-        #> PolyML.makestring (* FIXME *)
-        #> (fn s => report (Proof_Context.init_global thy) (PolyML.makestring file ^ " === " ^ s ^
-             " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> PolyML.makestring))))
+        #> @{make_string} (* FIXME *)
+        #> (fn s => report (Proof_Context.init_global thy) (@{make_string} file ^ " === " ^ s ^
+             " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> @{make_string}))))
        file
     end
 *}
 
 ML {*

        (fn prob_name =>
         (can
           (TPTP_Reconstruct.reconstruct ctxt (fn prob_name =>
             TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference prob_name (* oracle_based_reconstruction_tac *))) prob_name )
        |> (fn s => report ctxt (Path.print file ^ " === " ^ Bool.toString s ^
-             " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> PolyML.makestring))))
+             " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> @{make_string}))))
        prob_name
     end
 *}
 
 ML {*