# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID e5a23ffb5524d331b72cddc27d9a582c85146c53
# Parent  5c2f16eae066c966cefc2c016e0bd5be5bbcd2b0
improve precision of forall in constancy part of the monotonicity calculus

diff -r 5c2f16eae066 -r e5a23ffb5524 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:33:09 2010 +0100
@@ -113,9 +113,9 @@
 ML {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
 ML {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
 ML {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
+ML {* const @{term "\<forall>a\<Colon>'a. P a"} *}
 
 ML {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
-ML {* nonconst @{term "\<forall>a\<Colon>'a. P a"} *}
 ML {* nonconst @{term "THE x\<Colon>'a. P x"} *}
 ML {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
 ML {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
@@ -199,9 +199,9 @@
   in thy |> theorems_of |> List.app check_theorem end
 *}
 
-(*
 ML {* getenv "ISABELLE_TMP" *}
 
+(*
 (* ML {* check_theory @{theory AVL2} *} *)
 ML {* check_theory @{theory Fun} *}
 (* ML {* check_theory @{theory Huffman} *} *)
diff -r 5c2f16eae066 -r e5a23ffb5524 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
@@ -790,10 +790,11 @@
     fun do_all T (gamma, cset) =
       let
         val abs_M = mtype_for (domain_type (domain_type T))
+        val x = Unsynchronized.inc max_fresh
         val body_M = mtype_for (body_type T)
       in
-        (MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M),
-         (gamma, cset |> add_mtype_is_complete [] abs_M))
+        (MFun (MFun (abs_M, V x, body_M), A Gen, body_M),
+         (gamma, cset |> add_mtype_is_complete [(x, (Plus, Tru))] abs_M))
       end
     fun do_equals T (gamma, cset) =
       let