src/HOL/Tools/Nitpick/nitpick.ML
changeset 41793 c7a2669ae75d
parent 41791 01d722707a36
child 41801 ed77524f3429
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 10:44:19 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 11:50:31 2011 +0100
     1.3 @@ -363,6 +363,8 @@
     1.4          SOME (SOME b) => b
     1.5        | _ => is_type_fundamentally_monotonic T orelse
     1.6               is_type_actually_monotonic T
     1.7 +    fun is_deep_datatype_finitizable T =
     1.8 +      triple_lookup (type_match thy) finitizes T = SOME (SOME true)
     1.9      fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    1.10          is_type_kind_of_monotonic T
    1.11        | is_shallow_datatype_finitizable T =
    1.12 @@ -407,8 +409,10 @@
    1.13        all_Ts |> filter (is_datatype ctxt stds)
    1.14               |> List.partition is_datatype_deep
    1.15      val finitizable_dataTs =
    1.16 -      shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
    1.17 -                     |> filter is_shallow_datatype_finitizable
    1.18 +      (deep_dataTs |> filter_out (is_finite_type hol_ctxt)
    1.19 +                   |> filter is_deep_datatype_finitizable) @
    1.20 +      (shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
    1.21 +                      |> filter is_shallow_datatype_finitizable)
    1.22      val _ =
    1.23        if verbose andalso not (null finitizable_dataTs) then
    1.24          pprint_v (K (monotonicity_message finitizable_dataTs
    1.25 @@ -735,8 +739,8 @@
    1.26          if max_solutions <= 0 then
    1.27            (found_really_genuine, 0, 0, donno)
    1.28          else
    1.29 -          case KK.solve_any_problem overlord deadline max_threads max_solutions
    1.30 -                                    (map fst problems) of
    1.31 +          case KK.solve_any_problem debug overlord deadline max_threads
    1.32 +                                    max_solutions (map fst problems) of
    1.33              KK.JavaNotInstalled =>
    1.34              (print_m install_java_message;
    1.35               (found_really_genuine, max_potential, max_genuine, donno + 1))