# HG changeset patch
# User wenzelm
# Date 1600970052 -7200
# Node ID 811d5eec65a6b4e5960452a79f3fbba9c024c9c6
# Parent  32d5e474633a671d8c5a883988100f66d45a7df9
tuned;

diff -r 32d5e474633a -r 811d5eec65a6 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu Sep 24 19:33:33 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Sep 24 19:54:12 2020 +0200
@@ -300,7 +300,7 @@
     val driver_path = Path.append dir (Path.basic "driver.sml")
     val out_path = Path.append dir (Path.basic "out")
     val driver = \<^verbatim>\<open>
-fun main prog_name =
+fun main () =
   let
     fun format (true, _) = \<close> ^ ML_Syntax.print_string successN ^ \<^verbatim>\<open> ^ "\n"
       | format (false, NONE) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ "\n"
@@ -382,7 +382,7 @@
     val driver_path = Path.append dir (Path.basic driverN)
     val driver =
       "structure Test = struct\n" ^
-      "fun main prog_name =\n" ^
+      "fun main () =\n" ^
       "  let\n" ^
       "    fun format_term NONE = \"\"\n" ^
       "      | format_term (SOME t) = t ();\n" ^