src/HOL/Tools/Mirabelle/mirabelle.ML
changeset 73852 adb34395b622
parent 73851 bb277f37c34a
child 73854 eab5cd9c7862
equal deleted inserted replaced
73851:bb277f37c34a 73852:adb34395b622
   207           |> map_index I
   207           |> map_index I
   208           |> maps make_commands
   208           |> maps make_commands
   209           |> map_index I
   209           |> map_index I
   210           |> maps (fn (n, command) =>
   210           |> maps (fn (n, command) =>
   211             let val (m, k) = Integer.div_mod (n + 1) mirabelle_stride in
   211             let val (m, k) = Integer.div_mod (n + 1) mirabelle_stride in
   212               if k = 0 andalso m <= mirabelle_max_calls then
   212               if k = 0 andalso (mirabelle_max_calls <= 0 orelse m <= mirabelle_max_calls) then
   213                 map (fn context => (context, command)) contexts
   213                 map (fn context => (context, command)) contexts
   214               else
   214               else
   215                 []
   215                 []
   216             end)
   216             end)
   217           |> Par_List.map (fn ((action, context), command) => apply_action action context command);
   217           |> Par_List.map (fn ((action, context), command) => apply_action action context command);