# HG changeset patch
# User wenzelm
# Date 1600968813 -7200
# Node ID 32d5e474633a671d8c5a883988100f66d45a7df9
# Parent  03628da91b0720cdd2f3cd2d7107a7f1ec48a921
tuned;

diff -r 03628da91b07 -r 32d5e474633a src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu Sep 24 19:04:47 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Sep 24 19:33:33 2020 +0200
@@ -299,18 +299,17 @@
     val code_path = Path.append dir (Path.basic "generated.sml")
     val driver_path = Path.append dir (Path.basic "driver.sml")
     val out_path = Path.append dir (Path.basic "out")
-    val string = ML_Syntax.print_string
     val driver = \<^verbatim>\<open>
 fun main prog_name =
   let
-    fun format (true, _) = \<close> ^ string successN ^ \<^verbatim>\<open> ^ "\n"
-      | format (false, NONE) = \<close> ^ string failureN ^ \<^verbatim>\<open> ^ "\n"
-      | format (false, SOME t) = \<close> ^ string failureN ^ \<^verbatim>\<open> ^ t () ^ "\n"
+    fun format (true, _) = \<close> ^ ML_Syntax.print_string successN ^ \<^verbatim>\<open> ^ "\n"
+      | format (false, NONE) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ "\n"
+      | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ t () ^ "\n"
     val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
     val result_text = \<close> ^
-      string start_markerN ^
+      ML_Syntax.print_string start_markerN ^
       \<^verbatim>\<open> ^ String.concat (map format result) ^ \<close> ^
-      string end_markerN ^ \<^verbatim>\<open>
+      ML_Syntax.print_string end_markerN ^ \<^verbatim>\<open>
     val out = BinIO.openOut \<close> ^ ML_Syntax.print_platform_path out_path ^ \<^verbatim>\<open>
     val _ = BinIO.output (out, Byte.stringToBytes result_text)
     val _ = BinIO.closeOut out