always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
authorblanchet
Tue Jan 03 18:33:18 2012 +0100 (2012-01-03 ago)
changeset 461031e35730bd869
parent 46102 b669437de253
child 46104 eb85282db54e
always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -398,7 +398,8 @@
     1.4            SOME (SOME b) => b
     1.5          | _ => is_type_kind_of_monotonic T
     1.6      fun is_datatype_deep T =
     1.7 -      not standard orelse T = nat_T orelse is_word_type T orelse
     1.8 +      not standard orelse T = @{typ unit} orelse T = nat_T orelse
     1.9 +      is_word_type T orelse
    1.10        exists (curry (op =) T o domain_type o type_of) sel_names
    1.11      val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
    1.12                   |> sort Term_Ord.typ_ord