diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -160,7 +160,7 @@
   let
     fun is_type_actually_monotonic T =
       Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
-    val free_Ts = fold Term.add_tfrees ((@) tsp) [] |> map TFree
+    val free_Ts = fold Term.add_tfrees ((op @) tsp) [] |> map TFree
     val (mono_free_Ts, nonmono_free_Ts) =
       Timeout.apply mono_timeout
           (List.partition is_type_actually_monotonic) free_Ts