# HG changeset patch
# User blanchet
# Date 1426453215 -3600
# Node ID 44dabb962e481061e43be29c019a3fc9ce8f9791
# Parent  d4ce901f20c5eda9c8c8705e47f5b12f92d67d11
avoid controversial Pirate syntax

diff -r d4ce901f20c5 -r 44dabb962e48 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 14 21:16:29 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Mar 15 22:00:15 2015 +0100
@@ -2424,7 +2424,7 @@
              forall is_some ctrs')
           end
       in
-        ctrss |> map datatype_of_ctrs |> filter_out (null o #2)
+        ctrss |> map datatype_of_ctrs |> filter #3
       end
     else
       []