src/HOL/Library/code_test.ML

   val successN: string
   val failureN: string
   val start_markerN: string
   val end_markerN: string
   val test_terms: Proof.context -> term list -> string -> unit
-  val test_targets: Proof.context -> term list -> string list -> unit list
+  val test_targets: Proof.context -> term list -> string list -> unit
   val test_code_cmd: string list -> string list -> Toplevel.state -> unit
 
   val eval_term: string -> Proof.context -> term -> term
 
   val gen_driver:

   | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts)
 
 fun dest_tuples (Const (@{const_name Pair}, _) $ l $ r) = l :: dest_tuples r
   | dest_tuples t = [t]
 
-
-fun map_option _ NONE = NONE
-  | map_option f (SOME x) = SOME (f x)
 
 fun last_field sep str =
   let
     val n = size sep
     val len = size str

     val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
     fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
     fun evaluator program _ vs_ty deps =
       Exn.interruptible_capture evaluate
         (Code_Target.computation_text ctxt target program deps true vs_ty)
-    fun postproc f = map (apsnd (map_option (map f)))
+    fun postproc f = map (apsnd (Option.map (map f)))
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 
 
 (* term preprocessing *)
 

     fun ensure_bool t =
       (case fastype_of t of
         @{typ bool} => ()
       | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t)))
 
-    val _ = map ensure_bool ts
+    val _ = List.app ensure_bool ts
 
     val evals = map (fn t => filter term_of (add_eval t [])) ts
     val eval = map mk_term_of evals
 
-    val T =
-      HOLogic.mk_prodT (@{typ bool},
-        Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
-    val t = HOLogic.mk_list T (map HOLogic.mk_prod (ts ~~ eval))
+    val t =
+      HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
+        (map HOLogic.mk_prod (ts ~~ eval))
 
     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))
-    val _ = case failed of [] => ()
-      | _ => error (Pretty.string_of (pretty_failures ctxt target failed))
-  in
-    ()
-  end
-
-fun test_targets ctxt = map o test_terms ctxt
+  in
+    (case failed of [] =>
+      ()
+    | _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
+  end
+
+fun test_targets ctxt = List.app o test_terms ctxt
 
 fun test_code_cmd raw_ts targets state =
   let
     val ctxt = Toplevel.context_of state
     val ts = Syntax.read_terms ctxt raw_ts
     val frees = fold Term.add_free_names ts []
-    val _ = if frees = [] then () else
-      error ("Terms contain free variables: " ^
-      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
-  in
-    test_targets ctxt ts targets; ()
-  end
+    val _ =
+      if null frees then ()
+      else error ("Terms contain free variables: " ^
+        Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
+  in test_targets ctxt ts targets end
 
 fun eval_term target ctxt t =
   let
     val frees = Term.add_free_names t []
-    val _ = if frees = [] then () else
-      error ("Term contains free variables: " ^
-      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
+    val _ =
+      if null frees then ()
+      else error ("Term contains free variables: " ^
+        Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
 
     val thy = Proof_Context.theory_of ctxt
 
     val T_t = fastype_of t
-    val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error
-      ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^
+    val _ =
+      if Sign.of_sort thy (T_t, @{sort term_of}) then ()
+      else error ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^
        " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of}))
 
-    val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
-    val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
+    val t' =
+      HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
+        [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
 
     val result = dynamic_value_strict ctxt t' target
   in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
 
 

   let
     val compiler = getenv env_var
     val _ =
       if compiler <> "" then ()
       else error (Pretty.string_of (Pretty.para
-         ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
-         compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
+        ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
+          compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
 
     fun compile NONE = ()
       | compile (SOME cmd) =
           let
             val (out, ret) = Isabelle_System.bash_output cmd
           in
-            if ret = 0 then () else error
-              ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
+            if ret = 0 then ()
+            else error ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
           end
 
     fun run path =
       let
         val modules = map fst code_files
         val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt path modules value_name
 
-        val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files
-        val _ = map (fn (name, content) => File.write name content) files
+        val _ = List.app (fn (name, code) => File.write (mk_code_file name) code) code_files
+        val _ = List.app (fn (name, content) => File.write name content) files
 
         val _ = compile compile_cmd
 
         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)
+        val _ =
+          if res = 0 then ()
+          else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^
+            Int.toString res ^ "\nBash output:\n" ^ out)
       in out end
   in run end
 
 
 (* driver for PolyML *)