diff --git a/thys/SpecCheck/Output_Styles/output_style_custom.ML b/thys/SpecCheck/Output_Styles/output_style_custom.ML
--- a/thys/SpecCheck/Output_Styles/output_style_custom.ML
+++ b/thys/SpecCheck/Output_Styles/output_style_custom.ML
@@ -1,83 +1,96 @@
 (*  Title:      SpecCheck/Output_Style/output_style_custom.ML
     Author:     Lukas Bulwahn, Nicolai Schaffroth, Kevin Kappelmann TU Muenchen
     Author:     Christopher League
 
 Custom-made, QuickCheck-inspired output style for SpecCheck.
 *)
 
-structure SpecCheck_Output_Style_Custom : SPECCHECK_OUTPUT_STYLE =
+signature SPECCHECK_OUTPUT_STYLE_CUSTOM =
+sig
+  include SPECCHECK_OUTPUT_STYLE
+  val style_custom : (string -> unit) -> (string -> unit) ->
+    'a SpecCheck_Output_Style_Types.output_style
+end
+
+structure SpecCheck_Output_Style_Custom : SPECCHECK_OUTPUT_STYLE_CUSTOM =
 struct
 
 open SpecCheck_Base
 
-fun print_success stats =
+fun print_success writeln_info stats =
   let
     val num_success_tests = string_of_int (#num_success_tests stats)
     val num_discarded_tests = #num_discarded_tests stats
     val discarded_str =
       if num_discarded_tests = 0
       then "."
       else SpecCheck_Util.spaces [";", string_of_int num_discarded_tests,  "discarded."]
   in
     implode ["OK, passed ", num_success_tests, " tests", discarded_str]
-    |> writeln
+    |> writeln_info
   end
 
-fun print_gave_up stats =
+fun print_gave_up writeln_warning stats =
   let
     val num_success_tests = string_of_int (#num_success_tests stats)
     val num_discarded_tests = string_of_int (#num_discarded_tests stats)
   in
     SpecCheck_Util.spaces ["Gave up! Passed only", num_success_tests, "test(s);", num_discarded_tests,
       "discarded test(s)."]
-    |> warning
+    |> writeln_warning
   end
 
-fun print_failure_data ctxt show_opt failure_data =
+fun print_failure_data writeln_warning ctxt show_opt failure_data =
   case #the_exception failure_data of
     SOME exn =>
       cat_lines ["Exception during test run:", exnMessage exn]
-      |> warning
+      |> writeln_warning
   | NONE => case show_opt of
       NONE => ()
     | SOME show =>
       let
         val sort_counterexamples = Config.get ctxt SpecCheck_Configuration.sort_counterexamples
         val maybe_sort = if sort_counterexamples then sort (int_ord o apply2 size) else I
         val counterexamples =
           #counterexamples failure_data
           |> map (Pretty.string_of o show)
           |> maybe_sort
-      in fold (fn x => fn _ => warning x) counterexamples () end
+      in fold (fn x => fn _ => writeln_warning x) counterexamples () end
 
-fun print_failure ctxt show_opt (stats, failure_data) =
+fun print_failure writeln_warning ctxt show_opt (stats, failure_data) =
   ((SpecCheck_Util.spaces ["Failed! Falsified (after", string_of_int (num_tests stats), "test(s) and ",
-    string_of_int (num_shrinks stats), "shrink(s)):"] |> warning);
-  print_failure_data ctxt show_opt failure_data)
+    string_of_int (num_shrinks stats), "shrink(s)):"] |> writeln_warning);
+  print_failure_data writeln_warning ctxt show_opt failure_data)
 
-fun print_stats ctxt stats total_time =
+fun print_stats writeln_info ctxt stats total_time =
   let
     val show_stats = Config.get ctxt SpecCheck_Configuration.show_stats
     (*the time spent in the test function in relation to the total time spent;
       the latter includes generating test cases and overhead from the framework*)
     fun show_time {elapsed, ...} =
       implode ["Time: ", Time.toString elapsed, "s (run) / ", Time.toString (#elapsed total_time),
         "s (total)"]
   in
     if not show_stats
     then ()
-    else writeln (show_time (#timing stats))
+    else writeln_info (show_time (#timing stats))
   end
 
-fun style show_opt ctxt name total_time result =
+fun style_custom writeln_info writeln_warning show_opt ctxt name total_time
+  result =
   let val stats = stats_of_result result
   in
-    writeln (SpecCheck_Util.spaces ["Testing:", name]);
+    writeln_info (SpecCheck_Util.spaces ["Testing:", name]);
     (case result of
-      Success _ => print_success stats
-    | Gave_Up _ => print_gave_up stats
-    | Failure data => print_failure ctxt show_opt data);
-    print_stats ctxt stats total_time
+      Success _ => print_success writeln_info stats
+    | Gave_Up _ => print_gave_up writeln_warning stats
+    | Failure data => print_failure writeln_warning ctxt show_opt data);
+    print_stats writeln_info ctxt stats total_time
   end
 
+(*pass `error` instead of `warning` to make builds fail on test failure.
+TODO: passing `error` will block subsequent message printing; in particular,
+the failed test case will not be printed to the build log.*)
+fun style show_opt = style_custom writeln warning show_opt
+
 end
diff --git a/thys/SpecCheck/README.md b/thys/SpecCheck/README.md
--- a/thys/SpecCheck/README.md
+++ b/thys/SpecCheck/README.md
@@ -1,59 +1,63 @@
 # SpecCheck
 
 SpecCheck is a [QuickCheck](https://en.wikipedia.org/wiki/QuickCheck)-like testing framework for Isabelle/ML.
 You can use it to write specifications for ML functions.
 SpecCheck then checks whether your specification holds by testing your function against a given number of generated inputs.
 It helps you to identify bugs by printing counterexamples on failure and provides you timing information.
 
 SpecCheck is customisable and allows you to specify your own input generators,
 test output formats, as well as pretty printers and shrinking functions for counterexamples
 among other things.
 
 ## Quick Usage
 1. Import `SpecCheck.SpecCheck` into your environment.
 2. Write specifications using the ML invocation: `check show gen name prop ctxt seed` where
   * `show` converts values into `Pretty.T` types to show the failing inputs. See `show/`.
   * `gen` is the value generator used for the test. See `generators/`.
   * `name` is the name of the test case
   * `prop` is the property to be tested. See `property.ML`
   * `seed` is the initial seed for the generator.
 
 You can also choose to omit the show method for rapid testing or add a shrinking method à la
-QuickCheck to get better counterexamples. See `speccheck.ML`.
+QuickCheck to get better counterexamples.
+If you want to write unit tests, use `check_list` instead of `check`.
+A somewhat extensive example application can be found
+[here](https://github.com/kappelmann/e-unification-isabelle/blob/master/Tests/first_order_unification_tests.ML).
+For more information see `speccheck.ML`.
 
 An experimental alternative allows you to specify tests using strings:
 1. Import `SpecCheck_Dynamic.Dynamic` into your environment.
 2. `check_property "ALL x. P x"` where `P x` is some ML code evaluating to a boolean
 
-## Notes
+## Implementation Notes
 
 SpecCheck is based on [QCheck](https://github.com/league/qcheck), a testing framework for Standard ML by
 [Christopher League](https://contrapunctus.net/league/).
 As Isabelle/ML provides a rich and uniform ML platform, some features where removed or adapted, in particular:
 
 1. Isabelle/ML provides common data structures, which we can use in the
 tool's implementation for storing data and printing output.
 
 2. Implementations in Isabelle/ML checked with this tool commonly use Isabelle/ML's `int` type
 (which corresponds ML's `IntInf.int`), but do not use other integer types in ML such as ML's `Int.int`,
 `Word.word`, and others.
 
 3. As Isabelle makes heavy use of parallelism, we avoid reference types.
 
 ## Next Steps
 
 * Implement more shrinking methods for commonly used types
 * Implement sizing methods (cf. QuickCheck's `sized`)
 
 ## License
 
 The source code originated from Christopher League's QCheck, which is
 licensed under the 2-clause BSD license. The current source code is
 licensed under the compatible 3-clause BSD license of Isabelle.
 
 ## Authors
 
 * Lukas Bulwahn
 * Nicolai Schaffroth
 * Sebastian Willenbrink
 * Kevin Kappelmann