--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Nov 24 12:35:13 2014 +0100
@@ -49,7 +49,6 @@
Or |
And |
Less |
- Subset |
DefEq |
Eq |
Triad |
@@ -162,7 +161,6 @@
Or |
And |
Less |
- Subset |
DefEq |
Eq |
Triad |
@@ -225,7 +223,6 @@
| string_for_op2 Or = "Or"
| string_for_op2 And = "And"
| string_for_op2 Less = "Less"
- | string_for_op2 Subset = "Subset"
| string_for_op2 DefEq = "DefEq"
| string_for_op2 Eq = "Eq"
| string_for_op2 Triad = "Triad"
@@ -567,9 +564,7 @@
do_apply t0 ts
| (t0 as Const (x as (@{const_name ord_class.less_eq}, T)),
ts as [t1, t2]) =>
- if is_set_like_type (domain_type T) then
- Op2 (Subset, bool_T, Any, sub t1, sub t2)
- else if is_built_in_const x then
+ if is_built_in_const 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
@@ -914,21 +909,6 @@
val u2 = sub u2
val R = bool_rep polar (exists (is_opt_rep o rep_of) [u1, u2])
in s_op2 Less T R u1 u2 end
- | Op2 (Subset, T, _, u1, u2) =>
- let
- val u1 = sub u1
- val u2 = sub u2
- val opt = exists (is_opt_rep o rep_of) [u1, u2]
- val R = bool_rep polar opt
- in
- if is_opt_rep R then
- triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
- else if not opt orelse unsound orelse polar = Neg orelse
- is_concrete_type data_types true (type_of u1) then
- s_op2 Subset T R u1 u2
- else
- Cst (False, T, Formula Pos)
- end
| Op2 (DefEq, T, _, u1, u2) =>
s_op2 DefEq T (Formula Neut) (sub u1) (sub u2)
| Op2 (Eq, T, _, u1, u2) =>