src/HOL/Library/code_test.ML

   let
     val thy = Proof_Context.theory_of ctxt
     val (driver, target) =
       (case get_driver thy compiler of
         NONE => error ("No driver for target " ^ compiler)
-      | SOME f => f)
+      | SOME drv => drv)
     val debug = Config.get (Proof_Context.init_global thy) overlord
     val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
     fun evaluate result =
       with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
       |> parse_result compiler

     val result = dynamic_value_strict ctxt t target
 
     val failed =
       filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
       handle ListPair.UnequalLengths =>
-        error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
+        error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result))
   in
     (case failed of [] =>
       ()
     | _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
   end

 
         val (out, res) = Isabelle_System.bash_output run_cmd
         val _ =
           if res = 0 then ()
           else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^
-            Int.toString res ^ "\nBash output:\n" ^ out)
+            string_of_int res ^ "\nBash output:\n" ^ out)
       in out end
   in run end
 
 
 (* driver for PolyML *)

 
     fun mk_code_file name = Path.append path (Path.basic name)
     val driver_path = Path.append path (Path.basic driverN)
     val driver =
       "module Main where {\n" ^
-      String.concat (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
+      implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
       "main = do {\n" ^
       "    let {\n" ^
       "      format_term Nothing = \"\";\n" ^
       "      format_term (Just t) = t ();\n" ^
       "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^

         >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of)))
 
 val target_Scala = "Scala_eval"
 val target_Haskell = "Haskell_eval"
 
-val _ = Theory.setup 
+val _ = Theory.setup
    (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)])
     #> Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)]))
 
 val _ =
   Theory.setup (fold add_driver