Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 39342 1a0e6f16a91b
parent 39316 b6c4385ab400
child 39345 062c10ff848c 
--- 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
isabelle