1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jun 01 11:58:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jun 01 12:20:08 2010 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4       show_consts: bool,
     1.5       evals: term list,
     1.6       formats: (term option * int list) list,
     1.7 +     atomss: (typ option * string list) list,
     1.8       max_potential: int,
     1.9       max_genuine: int,
    1.10       check_potential: bool,
    1.11 @@ -112,6 +113,7 @@
    1.12     show_consts: bool,
    1.13     evals: term list,
    1.14     formats: (term option * int list) list,
    1.15 +   atomss: (typ option * string list) list,
    1.16     max_potential: int,
    1.17     max_genuine: int,
    1.18     check_potential: bool,
    1.19 @@ -190,7 +192,7 @@
    1.20           verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
    1.21           destroy_constrs, specialize, star_linear_preds, fast_descrs,
    1.22           peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
    1.23 -         evals, formats, max_potential, max_genuine, check_potential,
    1.24 +         evals, formats, atomss, max_potential, max_genuine, check_potential,
    1.25           check_genuine, batch_size, ...} = params
    1.26      val state_ref = Unsynchronized.ref state
    1.27      val pprint =
    1.28 @@ -575,8 +577,8 @@
    1.29          val (reconstructed_model, codatatypes_ok) =
    1.30            reconstruct_hol_model {show_datatypes = show_datatypes,
    1.31                                   show_consts = show_consts}
    1.32 -              scope formats frees free_names sel_names nonsel_names rel_table
    1.33 -              bounds
    1.34 +              scope formats atomss frees free_names sel_names nonsel_names
    1.35 +              rel_table bounds
    1.36          val genuine_means_genuine =
    1.37            got_all_user_axioms andalso none_true wfs andalso
    1.38            sound_finitizes andalso codatatypes_ok