src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 46083 efeaa79f021b
parent 46081 8f6465f7021b
child 46085 447cda88adfe
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
     1.3 @@ -745,7 +745,7 @@
     1.4          <= length ts
     1.5        | _ => true
     1.6      val mtype_for = fresh_mtype_for_type mdata false
     1.7 -    fun mtype_for_set x T = MFun (mtype_for (elem_type T), V x, bool_M)
     1.8 +    fun mtype_for_set x T = MFun (mtype_for (pseudo_domain_type T), V x, bool_M)
     1.9      fun do_all T (gamma, cset) =
    1.10        let
    1.11          val abs_M = mtype_for (domain_type (domain_type T))