# HG changeset patch
# User wenzelm
# Date 1613910785 -3600
# Node ID f5a77ee9106cd14a0c5992aa10bf7ab50c16cbbf
# Parent  c8abfe393c16e003ad76f5f23c01da7e74edec2c
proper treatment of process_result;

diff -r c8abfe393c16 -r f5a77ee9106c src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Feb 21 13:14:08 2021 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Feb 21 13:33:05 2021 +0100
@@ -283,7 +283,7 @@
                       string_of_int k))
               val _ = Quickcheck.add_timing timing current_result
             in
-              if response = "NONE\n" then with_size genuine_only (k + 1)
+              if response = "NONE" then with_size genuine_only (k + 1)
               else
                 let
                   val output_value = the_default "NONE"