src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 35219 15a5f213ef5b
parent 35190 ce653cc27a94
child 35220 2bcdae5f4fdb
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 08:17:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 10:38:37 2010 +0100
     1.3 @@ -189,7 +189,7 @@
     1.4    in List.app repair_one (!constr_cache) end
     1.5  
     1.6  (* cdata -> typ -> ctype *)
     1.7 -fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, alpha_T, max_fresh,
     1.8 +fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, binarize, alpha_T, max_fresh,
     1.9                             datatype_cache, constr_cache, ...} : cdata) =
    1.10    let
    1.11      (* typ -> typ -> ctype *)
    1.12 @@ -218,7 +218,7 @@
    1.13            | NONE =>
    1.14              let
    1.15                val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
    1.16 -              val xs = datatype_constrs hol_ctxt T
    1.17 +              val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
    1.18                val (all_Cs, constr_Cs) =
    1.19                  fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
    1.20                               let
    1.21 @@ -270,13 +270,8 @@
    1.22    if could_exist_alpha_sub_ctype thy alpha_T T then
    1.23      case AList.lookup (op =) (!constr_cache) x of
    1.24        SOME C => C
    1.25 -    | NONE => if T = alpha_T then
    1.26 -                let val C = fresh_ctype_for_type cdata T in
    1.27 -                  (Unsynchronized.change constr_cache (cons (x, C)); C)
    1.28 -                end
    1.29 -              else
    1.30 -                (fresh_ctype_for_type cdata (body_type T);
    1.31 -                 AList.lookup (op =) (!constr_cache) x |> the)
    1.32 +    | NONE => (fresh_ctype_for_type cdata (body_type T);
    1.33 +               AList.lookup (op =) (!constr_cache) x |> the)
    1.34    else
    1.35      fresh_ctype_for_type cdata T
    1.36  fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =