author | blanchet |
Mon, 13 Sep 2010 20:10:24 +0200 | |
changeset 39342 | 1a0e6f16a91b |
parent 39341 | d2b981a0429a |
child 39343 | eac5f82eefb6 |
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Sep 13 15:11:10 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Sep 13 20:10:24 2010 +0200 @@ -253,7 +253,7 @@ MAlpha else case T of Type (@{type_name fun}, [T1, T2]) => - MFun (fresh_mfun_for_fun_type mdata false T1 T2) + MFun (fresh_mfun_for_fun_type mdata all_minus T1 T2) | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2)) | Type (z as (s, _)) => if could_exist_alpha_sub_mtype ctxt alpha_T T then