Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
authorblanchet
Thu, 01 Mar 2012 11:28:56 +0100
changeset 46746 a10dcc985e8d
parent 46745 a6f83f21dc2c
child 46747 b91628b2522b
improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
src/HOL/Tools/Nitpick/nitpick_hol.ML file | annotate | diff | comparison | revisions 
--- 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},
isabelle