--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Jan 03 18:33:17 2012 +0100
@@ -68,7 +68,7 @@
by auto
lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1\<emdash>2, expect = none]
by auto
lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
@@ -147,7 +147,7 @@
nitpick [card = 15, expect = none]
by auto
-lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow>
+lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow>
A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
nitpick [card = 1\<emdash>25, expect = none]
by auto
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Jan 03 18:33:17 2012 +0100
@@ -1423,8 +1423,9 @@
| Atom (k, _) =>
let
val dom_card = card_of_rep (rep_of arg_u)
- val ran_R = Atom (exact_root dom_card k,
- offset_of_type ofs (range_type (type_of func_u)))
+ val ran_R =
+ Atom (exact_root dom_card k,
+ offset_of_type ofs (pseudo_range_type (type_of func_u)))
in
to_apply_vect dom_card ran_R res_R (to_vect dom_card ran_R func_u)
arg_u
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jan 03 18:33:17 2012 +0100
@@ -845,7 +845,7 @@
| @{const_name fst} => do_nth_pair_sel 0 T accum
| @{const_name snd} => do_nth_pair_sel 1 T accum
| @{const_name Id} =>
- (MFun (mtype_for (domain_type T), A Gen, bool_M), accum)
+ (MFun (mtype_for (elem_type T), A Gen, bool_M), accum)
| @{const_name converse} =>
let
val x = Unsynchronized.inc max_fresh
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jan 03 18:33:17 2012 +0100
@@ -562,11 +562,11 @@
do_apply t0 ts
| (t0 as Const (x as (@{const_name ord_class.less_eq}, T)),
ts as [t1, t2]) =>
- if is_built_in_const thy stds x then
+ if is_set_like_type (domain_type T) then
+ Op2 (Subset, bool_T, Any, sub t1, sub t2)
+ else if is_built_in_const thy stds x then
(* FIXME: find out if this case is necessary *)
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
- else if is_set_like_type (domain_type T) then
- Op2 (Subset, bool_T, Any, sub t1, sub t2)
else
do_apply t0 ts
| (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
@@ -968,7 +968,7 @@
val u2' = aux table' false Neut u2
val R =
if is_opt_rep (rep_of u2') orelse
- (range_type T = bool_T andalso
+ (pseudo_range_type T = bool_T andalso
not (is_Cst False (unrepify_nut_in_nut table false Neut
u1 u2))) then
opt_rep ofs T R
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Jan 03 18:33:17 2012 +0100
@@ -234,7 +234,8 @@
fun rep_to_binary_rel_rep ofs T R =
let
val k = exact_root 2 (card_of_domain_from_rep 2 R)
- val j0 = offset_of_type ofs (fst (HOLogic.dest_prodT (domain_type T)))
+ val j0 =
+ offset_of_type ofs (fst (HOLogic.dest_prodT (pseudo_domain_type T)))
in Func (Struct [Atom (k, j0), Atom (k, j0)], Formula Neut) end
fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)