src/HOL/Tools/Mirabelle/mirabelle.ML
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
                 []