changeset 73269 | f5a77ee9106c |
parent 72511 | 460d743010bc |
child 73283 | 057d8a164a7b |
--- 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"