changeset 73852 | adb34395b622 |
parent 73851 | bb277f37c34a |
child 73854 | eab5cd9c7862 |
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Sat Jun 12 12:39:33 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sat Jun 12 15:37:25 2021 +0200 @@ -209,7 +209,7 @@ |> map_index I |> maps (fn (n, command) => let val (m, k) = Integer.div_mod (n + 1) mirabelle_stride in - if k = 0 andalso m <= mirabelle_max_calls then + if k = 0 andalso (mirabelle_max_calls <= 0 orelse m <= mirabelle_max_calls) then map (fn context => (context, command)) contexts else []