# HG changeset patch
# User blanchet
# Date 1330597736 -3600
# Node ID a10dcc985e8d70232817a2c7487f36069ad45ecc
# Parent  a6f83f21dc2c1b39e1acb9301c57f8c3802fa45e
improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case

diff -r a6f83f21dc2c -r a10dcc985e8d src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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},