src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 35190 ce653cc27a94
parent 35185 9b8f351cced6
child 35220 2bcdae5f4fdb
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 14:11:41 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 20:46:50 2010 +0100
     1.3 @@ -747,10 +747,10 @@
     1.4  
     1.5  (* scope -> styp -> int -> nut list * rep NameTable.table
     1.6     -> nut list * rep NameTable.table *)
     1.7 -fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n
     1.8 -                                      (vs, table) =
     1.9 +fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
    1.10 +                                      (x as (_, T)) n (vs, table) =
    1.11    let
    1.12 -    val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n
    1.13 +    val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
    1.14      val R' = if n = ~1 orelse is_word_type (body_type T) orelse
    1.15                  (is_fun_type (range_type T') andalso
    1.16                   is_boolean_type (body_type T')) then