1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jun 01 15:59:01 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jun 01 17:52:19 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 @@ -235,14 +237,9 @@
    1.29                         |> pairf hd tl
    1.30      val original_max_potential = max_potential
    1.31      val original_max_genuine = max_genuine
    1.32 -(*
    1.33 -    val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t)
    1.34 -    val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t))
    1.35 -                     orig_assm_ts
    1.36 -*)
    1.37      val max_bisim_depth = fold Integer.max bisim_depths ~1
    1.38      val case_names = case_const_names thy stds
    1.39 -    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
    1.40 +    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
    1.41      val def_table = const_def_table ctxt subst defs
    1.42      val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
    1.43      val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
    1.44 @@ -322,8 +319,8 @@
    1.45          ". " ^ extra
    1.46        end
    1.47      fun is_type_fundamentally_monotonic T =
    1.48 -      (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
    1.49 -       (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
    1.50 +      (is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso
    1.51 +       (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
    1.52        is_number_type thy T orelse is_bit_type T
    1.53      fun is_type_actually_monotonic T =
    1.54        formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
    1.55 @@ -369,7 +366,8 @@
    1.56        else
    1.57          ()
    1.58      val (deep_dataTs, shallow_dataTs) =
    1.59 -      all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
    1.60 +      all_Ts |> filter (is_datatype ctxt stds)
    1.61 +             |> List.partition is_datatype_deep
    1.62      val finitizable_dataTs =
    1.63        shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
    1.64                       |> filter is_shallow_datatype_finitizable
    1.65 @@ -579,8 +577,8 @@
    1.66          val (reconstructed_model, codatatypes_ok) =
    1.67            reconstruct_hol_model {show_datatypes = show_datatypes,
    1.68                                   show_consts = show_consts}
    1.69 -              scope formats frees free_names sel_names nonsel_names rel_table
    1.70 -              bounds
    1.71 +              scope formats atomss frees free_names sel_names nonsel_names
    1.72 +              rel_table bounds
    1.73          val genuine_means_genuine =
    1.74            got_all_user_axioms andalso none_true wfs andalso
    1.75            sound_finitizes andalso codatatypes_ok