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, 03 Jan 2012 18:33:18 +0100
changeset 46103 1e35730bd869
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
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -398,7 +398,8 @@
           SOME (SOME b) => b
         | _ => is_type_kind_of_monotonic T
     fun is_datatype_deep T =
-      not standard orelse T = nat_T orelse is_word_type T orelse
+      not standard orelse T = @{typ unit} orelse T = nat_T orelse
+      is_word_type T orelse
       exists (curry (op =) T o domain_type o type_of) sel_names
     val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
                  |> sort Term_Ord.typ_ord