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