# HG changeset patch
# User blanchet
# Date 1266485917 -3600
# Node ID 15a5f213ef5b5d603fef04cc9cb53a222781b5b2
# Parent  5c5457a7be85732b4b209b310ab40621d682f694
fix bug in Nitpick's monotonicity code w.r.t. binary integers

diff -r 5c5457a7be85 -r 15a5f213ef5b src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 08:17:24 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 10:38:37 2010 +0100
@@ -189,7 +189,7 @@
   in List.app repair_one (!constr_cache) end
 
 (* cdata -> typ -> ctype *)
-fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, alpha_T, max_fresh,
+fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, binarize, alpha_T, max_fresh,
                            datatype_cache, constr_cache, ...} : cdata) =
   let
     (* typ -> typ -> ctype *)
@@ -218,7 +218,7 @@
           | NONE =>
             let
               val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
-              val xs = datatype_constrs hol_ctxt T
+              val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
               val (all_Cs, constr_Cs) =
                 fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
                              let
@@ -270,13 +270,8 @@
   if could_exist_alpha_sub_ctype thy alpha_T T then
     case AList.lookup (op =) (!constr_cache) x of
       SOME C => C
-    | NONE => if T = alpha_T then
-                let val C = fresh_ctype_for_type cdata T in
-                  (Unsynchronized.change constr_cache (cons (x, C)); C)
-                end
-              else
-                (fresh_ctype_for_type cdata (body_type T);
-                 AList.lookup (op =) (!constr_cache) x |> the)
+    | NONE => (fresh_ctype_for_type cdata (body_type T);
+               AList.lookup (op =) (!constr_cache) x |> the)
   else
     fresh_ctype_for_type cdata T
 fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =