src/HOL/Tools/Nitpick/nitpick.ML
changeset 41052 3db267a01c1d
parent 41051 2ed1b971fc20
child 41278 8e1cde88aae6
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:53 2010 +0100
     1.3 @@ -292,7 +292,7 @@
     1.4      val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
     1.5              raise NOT_SUPPORTED "schematic type variables"
     1.6      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
     1.7 -         binarize) = preprocess_formulas hol_ctxt finitizes monos assm_ts neg_t
     1.8 +         binarize) = preprocess_formulas hol_ctxt assm_ts neg_t
     1.9      val got_all_user_axioms =
    1.10        got_all_mono_user_axioms andalso no_poly_user_axioms
    1.11  
    1.12 @@ -361,9 +361,7 @@
    1.13          SOME (SOME b) => b
    1.14        | _ => is_type_fundamentally_monotonic T orelse
    1.15               is_type_actually_monotonic T
    1.16 -    fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
    1.17 -        is_type_kind_of_monotonic T
    1.18 -      | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    1.19 +    fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    1.20          is_type_kind_of_monotonic T
    1.21        | is_shallow_datatype_finitizable T =
    1.22          case triple_lookup (type_match thy) finitizes T of