src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 36384 76d5fd5a45fb
parent 35866 513074557e06
child 36385 ff5f88702590
equal deleted inserted replaced
36383:6adf1068ac0f 36384:76d5fd5a45fb
    81         if is_built_in_const thy [(NONE, true)] true x orelse
    81         if is_built_in_const thy [(NONE, true)] true x orelse
    82            is_constr_like thy x orelse
    82            is_constr_like thy x orelse
    83            is_sel s orelse s = @{const_name Sigma} then
    83            is_sel s orelse s = @{const_name Sigma} then
    84           table
    84           table
    85         else
    85         else
    86           Termtab.map_default (t, 65536) (curry Int.min (length args)) table
    86           Termtab.map_default (t, 65536) (Integer.min (length args)) table
    87       | aux _ _ table = table
    87       | aux _ _ table = table
    88   in aux t [] end
    88   in aux t [] end
    89 
    89 
    90 (* int -> int -> string *)
    90 (* int -> int -> string *)
    91 fun uncurry_prefix_for k j =
    91 fun uncurry_prefix_for k j =