proper treatment of process_result;
authorwenzelm
Sun, 21 Feb 2021 13:33:05 +0100
changeset 73269 f5a77ee9106c
parent 73268 c8abfe393c16
child 73270 e2d03448d5b5
child 73273 17c28251fff0
child 73302 915b3d41dec1
proper treatment of process_result;
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"