src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 45797 977cf00fb8d3
parent 45280 9fd6fce8a230
child 45980 af59825c40cf
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 09 14:12:02 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 09 14:14:37 2011 +0100
     1.3 @@ -720,12 +720,12 @@
     1.4    | is_rep_fun _ _ = false
     1.5  fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
     1.6                                           [_, abs_T as Type (s', _)]))) =
     1.7 -    try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
     1.8 +    try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
     1.9      = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
    1.10    | is_quot_abs_fun _ _ = false
    1.11  fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun},
    1.12                                           [abs_T as Type (s', _), _]))) =
    1.13 -    try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
    1.14 +    try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) s'
    1.15      = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
    1.16    | is_quot_rep_fun _ _ = false
    1.17