improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 01 11:28:56 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 01 11:28:56 2012 +0100
@@ -744,10 +744,11 @@
try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
= SOME (Const x) andalso not (is_codatatype ctxt abs_T)
| is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun},
- [abs_T as Type (s', _), _]))) =
- try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) s'
- = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
+fun is_quot_rep_fun ctxt (x as (s, Type (@{type_name fun},
+ [abs_T as Type (abs_s, _), _]))) =
+ (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
+ SOME (Const (s', _)) => s = s' andalso not (is_codatatype ctxt abs_T)
+ | NONE => false)
| is_quot_rep_fun _ _ = false
fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},