--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 12 21:27:06 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Feb 13 11:56:06 2010 +0100
@@ -22,6 +22,7 @@
typ: typ,
card: int,
co: bool,
+ standard: bool,
complete: bool,
concrete: bool,
deep: bool,
@@ -71,6 +72,7 @@
typ: typ,
card: int,
co: bool,
+ standard: bool,
complete: bool,
concrete: bool,
deep: bool,
@@ -466,6 +468,7 @@
let
val deep = member (op =) deep_dataTs T
val co = is_codatatype thy T
+ val standard = is_standard_datatype hol_ctxt T
val xs = boxed_datatype_constrs hol_ctxt T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
@@ -481,8 +484,8 @@
num_non_self_recs)
(sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
in
- {typ = T, card = card, co = co, complete = complete, concrete = concrete,
- deep = deep, constrs = constrs}
+ {typ = T, card = card, co = co, standard = standard, complete = complete,
+ concrete = concrete, deep = deep, constrs = constrs}
end
(* int -> int *)