src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 39342 1a0e6f16a91b
parent 39316 b6c4385ab400
child 39345 062c10ff848c
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Sep 13 15:11:10 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Sep 13 20:10:24 2010 +0200
     1.3 @@ -253,7 +253,7 @@
     1.4          MAlpha
     1.5        else case T of
     1.6          Type (@{type_name fun}, [T1, T2]) =>
     1.7 -        MFun (fresh_mfun_for_fun_type mdata false T1 T2)
     1.8 +        MFun (fresh_mfun_for_fun_type mdata all_minus T1 T2)
     1.9        | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
    1.10        | Type (z as (s, _)) =>
    1.11          if could_exist_alpha_sub_mtype ctxt alpha_T T then