src/HOL/Library/code_test.ML

     val code = #2 (the_single code_files);
     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 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"
       | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ t () ^ "\n"
     val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()

 
     val code_path = Path.append dir (Path.basic generatedN)
     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" ^
       "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
       "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^