always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
authorblanchet
Mon Feb 21 10:42:29 2011 +0100 (2011-02-21)
changeset 4179101d722707a36
parent 41790 56dcd46ddf7a
child 41792 ff3cb0c418b7
always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 21 10:31:48 2011 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 21 10:42:29 2011 +0100
     1.3 @@ -24,14 +24,14 @@
     1.4  val subst = []
     1.5  val case_names = case_const_names ctxt stds
     1.6  val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
     1.7 -val def_table = const_def_table ctxt subst defs
     1.8 +val def_tables = const_def_tables ctxt subst defs
     1.9  val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
    1.10  val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
    1.11  val psimp_table = const_psimp_table ctxt subst
    1.12  val choice_spec_table = const_choice_spec_table ctxt subst
    1.13  val user_nondefs =
    1.14    user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
    1.15 -val intro_table = inductive_intro_table ctxt subst def_table
    1.16 +val intro_table = inductive_intro_table ctxt subst def_tables
    1.17  val ground_thm_table = ground_theorem_table thy
    1.18  val ersatz_table = ersatz_table ctxt
    1.19  val hol_ctxt as {thy, ...} : hol_context =
    1.20 @@ -40,7 +40,7 @@
    1.21     whacks = [], binary_ints = SOME false, destroy_constrs = true,
    1.22     specialize = false, star_linear_preds = false,
    1.23     tac_timeout = NONE, evals = [], case_names = case_names,
    1.24 -   def_table = def_table, nondef_table = nondef_table,
    1.25 +   def_tables = def_tables, nondef_table = nondef_table,
    1.26     user_nondefs = user_nondefs, simp_table = simp_table,
    1.27     psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    1.28     intro_table = intro_table, ground_thm_table = ground_thm_table,
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 10:31:48 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 10:42:29 2011 +0100
     2.3 @@ -265,14 +265,14 @@
     2.4      val max_bisim_depth = fold Integer.max bisim_depths ~1
     2.5      val case_names = case_const_names ctxt stds
     2.6      val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
     2.7 -    val def_table = const_def_table ctxt subst defs
     2.8 +    val def_tables = const_def_tables ctxt subst defs
     2.9      val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
    2.10      val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
    2.11      val psimp_table = const_psimp_table ctxt subst
    2.12      val choice_spec_table = const_choice_spec_table ctxt subst
    2.13      val user_nondefs =
    2.14        user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
    2.15 -    val intro_table = inductive_intro_table ctxt subst def_table
    2.16 +    val intro_table = inductive_intro_table ctxt subst def_tables
    2.17      val ground_thm_table = ground_theorem_table thy
    2.18      val ersatz_table = ersatz_table ctxt
    2.19      val hol_ctxt as {wf_cache, ...} =
    2.20 @@ -281,7 +281,7 @@
    2.21         whacks = whacks, binary_ints = binary_ints,
    2.22         destroy_constrs = destroy_constrs, specialize = specialize,
    2.23         star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
    2.24 -       evals = evals, case_names = case_names, def_table = def_table,
    2.25 +       evals = evals, case_names = case_names, def_tables = def_tables,
    2.26         nondef_table = nondef_table, user_nondefs = user_nondefs,
    2.27         simp_table = simp_table, psimp_table = psimp_table,
    2.28         choice_spec_table = choice_spec_table, intro_table = intro_table,
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 10:31:48 2011 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 10:42:29 2011 +0100
     3.3 @@ -30,7 +30,7 @@
     3.4       tac_timeout: Time.time option,
     3.5       evals: term list,
     3.6       case_names: (string * int) list,
     3.7 -     def_table: const_table,
     3.8 +     def_tables: const_table * const_table,
     3.9       nondef_table: const_table,
    3.10       user_nondefs: term list,
    3.11       simp_table: const_table Unsynchronized.ref,
    3.12 @@ -187,15 +187,17 @@
    3.13    val case_const_names :
    3.14      Proof.context -> (typ option * bool) list -> (string * int) list
    3.15    val unfold_defs_in_term : hol_context -> term -> term
    3.16 -  val const_def_table :
    3.17 -    Proof.context -> (term * term) list -> term list -> const_table
    3.18 +  val const_def_tables :
    3.19 +    Proof.context -> (term * term) list -> term list
    3.20 +    -> const_table * const_table
    3.21    val const_nondef_table : term list -> const_table
    3.22    val const_simp_table : Proof.context -> (term * term) list -> const_table
    3.23    val const_psimp_table : Proof.context -> (term * term) list -> const_table
    3.24    val const_choice_spec_table :
    3.25      Proof.context -> (term * term) list -> const_table
    3.26    val inductive_intro_table :
    3.27 -    Proof.context -> (term * term) list -> const_table -> const_table
    3.28 +    Proof.context -> (term * term) list -> const_table * const_table
    3.29 +    -> const_table
    3.30    val ground_theorem_table : theory -> term list Inttab.table
    3.31    val ersatz_table : Proof.context -> (string * string) list
    3.32    val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
    3.33 @@ -203,10 +205,10 @@
    3.34    val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
    3.35    val optimized_quot_type_axioms :
    3.36      Proof.context -> (typ option * bool) list -> string * typ list -> term list
    3.37 -  val def_of_const : theory -> const_table -> styp -> term option
    3.38 +  val def_of_const : theory -> const_table * const_table -> styp -> term option
    3.39    val fixpoint_kind_of_rhs : term -> fixpoint_kind
    3.40    val fixpoint_kind_of_const :
    3.41 -    theory -> const_table -> string * typ -> fixpoint_kind
    3.42 +    theory -> const_table * const_table -> string * typ -> fixpoint_kind
    3.43    val is_real_inductive_pred : hol_context -> styp -> bool
    3.44    val is_constr_pattern_lhs : Proof.context -> term -> bool
    3.45    val is_constr_pattern_formula : Proof.context -> term -> bool
    3.46 @@ -256,7 +258,7 @@
    3.47     tac_timeout: Time.time option,
    3.48     evals: term list,
    3.49     case_names: (string * int) list,
    3.50 -   def_table: const_table,
    3.51 +   def_tables: const_table * const_table,
    3.52     nondef_table: const_table,
    3.53     user_nondefs: term list,
    3.54     simp_table: const_table Unsynchronized.ref,
    3.55 @@ -1376,14 +1378,19 @@
    3.56      val args = strip_comb lhs |> snd
    3.57    in fold_rev aux args (SOME rhs) end
    3.58  
    3.59 -fun def_of_const thy table (x as (s, _)) =
    3.60 -  if is_built_in_const thy [(NONE, false)] x orelse
    3.61 -     original_name s <> s then
    3.62 +fun get_def_of_const thy table (x as (s, _)) =
    3.63 +  x |> def_props_for_const thy [(NONE, false)] table |> List.last
    3.64 +    |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
    3.65 +  handle List.Empty => NONE
    3.66 +
    3.67 +fun def_of_const_ext thy (unfold_table, fallback_table) (x as (s, _)) =
    3.68 +  if is_built_in_const thy [(NONE, false)] x orelse original_name s <> s then
    3.69      NONE
    3.70 -  else
    3.71 -    x |> def_props_for_const thy [(NONE, false)] table |> List.last
    3.72 -      |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
    3.73 -    handle List.Empty => NONE
    3.74 +  else case get_def_of_const thy unfold_table x of
    3.75 +    SOME def => SOME (true, def)
    3.76 +  | NONE => get_def_of_const thy fallback_table x |> Option.map (pair false)
    3.77 +
    3.78 +val def_of_const = Option.map snd ooo def_of_const_ext
    3.79  
    3.80  fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
    3.81    | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
    3.82 @@ -1434,9 +1441,9 @@
    3.83    else fixpoint_kind_of_rhs (the (def_of_const thy table x))
    3.84    handle Option.Option => NoFp
    3.85  
    3.86 -fun is_real_inductive_pred ({thy, stds, def_table, intro_table, ...}
    3.87 +fun is_real_inductive_pred ({thy, stds, def_tables, intro_table, ...}
    3.88                              : hol_context) x =
    3.89 -  fixpoint_kind_of_const thy def_table x <> NoFp andalso
    3.90 +  fixpoint_kind_of_const thy def_tables x <> NoFp andalso
    3.91    not (null (def_props_for_const thy stds intro_table x))
    3.92  fun is_inductive_pred hol_ctxt (x as (s, _)) =
    3.93    is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
    3.94 @@ -1502,11 +1509,11 @@
    3.95    #> Object_Logic.atomize_term thy
    3.96    #> Choice_Specification.close_form
    3.97    #> HOLogic.mk_Trueprop
    3.98 -fun is_choice_spec_fun ({thy, def_table, nondef_table, choice_spec_table, ...}
    3.99 +fun is_choice_spec_fun ({thy, def_tables, nondef_table, choice_spec_table, ...}
   3.100                          : hol_context) x =
   3.101    case nondef_props_for_const thy true choice_spec_table x of
   3.102      [] => false
   3.103 -  | ts => case def_of_const thy def_table x of
   3.104 +  | ts => case def_of_const thy def_tables x of
   3.105              SOME (Const (@{const_name Eps}, _) $ _) => true
   3.106            | SOME _ => false
   3.107            | NONE =>
   3.108 @@ -1614,7 +1621,7 @@
   3.109  val def_inline_threshold_for_non_booleans = 20
   3.110  
   3.111  fun unfold_defs_in_term
   3.112 -        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_table,
   3.113 +        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_tables,
   3.114                        ground_thm_table, ersatz_table, ...}) =
   3.115    let
   3.116      fun do_term depth Ts t =
   3.117 @@ -1781,8 +1788,8 @@
   3.118                else if is_equational_fun_but_no_plain_def hol_ctxt x orelse
   3.119                        is_choice_spec_fun hol_ctxt x then
   3.120                  (Const x, ts)
   3.121 -              else case def_of_const thy def_table x of
   3.122 -                SOME def =>
   3.123 +              else case def_of_const_ext thy def_tables x of
   3.124 +                SOME (unfold, def) =>
   3.125                  if depth > unfold_max_depth then
   3.126                    raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
   3.127                                     "too many nested definitions (" ^
   3.128 @@ -1790,7 +1797,8 @@
   3.129                                     quote s)
   3.130                  else if s = @{const_name wfrec'} then
   3.131                    (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
   3.132 -                else if size_of_term def > def_inline_threshold () then
   3.133 +                else if not unfold andalso
   3.134 +                     size_of_term def > def_inline_threshold () then
   3.135                    (Const x, ts)
   3.136                  else
   3.137                    (do_term (depth + 1) Ts def, ts)
   3.138 @@ -1841,10 +1849,10 @@
   3.139    ctxt |> get |> map (pair_for_prop o subst_atomic subst)
   3.140         |> AList.group (op =) |> Symtab.make
   3.141  
   3.142 -fun const_def_table ctxt subst ts =
   3.143 -  def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst
   3.144 -  |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
   3.145 -          (map pair_for_prop ts)
   3.146 +fun const_def_tables ctxt subst ts =
   3.147 +  (def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst,
   3.148 +   fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
   3.149 +        (map pair_for_prop ts) Symtab.empty)
   3.150  
   3.151  fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
   3.152  fun const_nondef_table ts =
   3.153 @@ -1861,10 +1869,10 @@
   3.154    map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
   3.155    |> const_nondef_table
   3.156  
   3.157 -fun inductive_intro_table ctxt subst def_table =
   3.158 +fun inductive_intro_table ctxt subst def_tables =
   3.159    let val thy = ProofContext.theory_of ctxt in
   3.160      def_table_for
   3.161 -        (maps (map (unfold_mutually_inductive_preds thy def_table o prop_of)
   3.162 +        (maps (map (unfold_mutually_inductive_preds thy def_tables o prop_of)
   3.163                 o snd o snd)
   3.164           o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
   3.165                                    cat = Spec_Rules.Co_Inductive)
   3.166 @@ -2086,7 +2094,7 @@
   3.167  (* The type constraint below is a workaround for a Poly/ML crash. *)
   3.168  
   3.169  fun is_well_founded_inductive_pred
   3.170 -        (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
   3.171 +        (hol_ctxt as {thy, wfs, def_tables, wf_cache, ...} : hol_context)
   3.172          (x as (s, _)) =
   3.173    case triple_lookup (const_match thy) wfs x of
   3.174      SOME (SOME b) => b
   3.175 @@ -2095,7 +2103,7 @@
   3.176             SOME (_, wf) => wf
   3.177           | NONE =>
   3.178             let
   3.179 -             val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   3.180 +             val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
   3.181               val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
   3.182             in
   3.183               Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
   3.184 @@ -2214,13 +2222,13 @@
   3.185    | is_good_starred_linear_pred_type _ = false
   3.186  
   3.187  fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
   3.188 -                                                def_table, simp_table, ...})
   3.189 +                                                def_tables, simp_table, ...})
   3.190                                    gfp (x as (s, T)) =
   3.191    let
   3.192      val iter_T = iterator_type_for_const gfp x
   3.193      val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
   3.194      val unrolled_const = Const x' $ zero_const iter_T
   3.195 -    val def = the (def_of_const thy def_table x)
   3.196 +    val def = the (def_of_const thy def_tables x)
   3.197    in
   3.198      if is_equational_fun_but_no_plain_def hol_ctxt x' then
   3.199        unrolled_const (* already done *)
   3.200 @@ -2251,9 +2259,9 @@
   3.201        in unrolled_const end
   3.202    end
   3.203  
   3.204 -fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
   3.205 +fun raw_inductive_pred_axiom ({thy, def_tables, ...} : hol_context) x =
   3.206    let
   3.207 -    val def = the (def_of_const thy def_table x)
   3.208 +    val def = the (def_of_const thy def_tables x)
   3.209      val (outer, fp_app) = strip_abs def
   3.210      val outer_bounds = map Bound (length outer - 1 downto 0)
   3.211      val rhs =
   3.212 @@ -2277,13 +2285,13 @@
   3.213    else
   3.214      raw_inductive_pred_axiom hol_ctxt x
   3.215  
   3.216 -fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_table, simp_table,
   3.217 +fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_tables, simp_table,
   3.218                                          psimp_table, ...}) x =
   3.219    case def_props_for_const thy stds (!simp_table) x of
   3.220      [] => (case def_props_for_const thy stds psimp_table x of
   3.221               [] => (if is_inductive_pred hol_ctxt x then
   3.222                        [inductive_pred_axiom hol_ctxt x]
   3.223 -                    else case def_of_const thy def_table x of
   3.224 +                    else case def_of_const thy def_tables x of
   3.225                        SOME def =>
   3.226                        @{const Trueprop} $ HOLogic.mk_eq (Const x, def)
   3.227                        |> equationalize_term ctxt "" |> the |> single
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 21 10:31:48 2011 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 21 10:42:29 2011 +0100
     4.3 @@ -662,9 +662,9 @@
     4.4    | dest_n_tuple_type _ T =
     4.5      raise TYPE ("Nitpick_Model.dest_n_tuple_type", [T], [])
     4.6  
     4.7 -fun const_format thy def_table (x as (s, T)) =
     4.8 +fun const_format thy def_tables (x as (s, T)) =
     4.9    if String.isPrefix unrolled_prefix s then
    4.10 -    const_format thy def_table (original_name s, range_type T)
    4.11 +    const_format thy def_tables (original_name s, range_type T)
    4.12    else if String.isPrefix skolem_prefix s then
    4.13      let
    4.14        val k = unprefix skolem_prefix s
    4.15 @@ -673,7 +673,7 @@
    4.16      in [k, num_binder_types T - k] end
    4.17    else if original_name s <> s then
    4.18      [num_binder_types T]
    4.19 -  else case def_of_const thy def_table x of
    4.20 +  else case def_of_const thy def_tables x of
    4.21      SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
    4.22                   let val k = length (strip_abs_vars t') in
    4.23                     [k, num_binder_types T - k]
    4.24 @@ -690,7 +690,7 @@
    4.25        [Int.min (k1, k2)]
    4.26      end
    4.27  
    4.28 -fun lookup_format thy def_table formats t =
    4.29 +fun lookup_format thy def_tables formats t =
    4.30    case AList.lookup (fn (SOME x, SOME y) =>
    4.31                          (term_match thy) (x, y) | _ => false)
    4.32                      formats (SOME t) of
    4.33 @@ -698,7 +698,7 @@
    4.34    | NONE => let val format = the (AList.lookup (op =) formats NONE) in
    4.35                case t of
    4.36                  Const x => intersect_formats format
    4.37 -                                             (const_format thy def_table x)
    4.38 +                                             (const_format thy def_tables x)
    4.39                | _ => format
    4.40              end
    4.41  
    4.42 @@ -719,16 +719,16 @@
    4.43            |> map (HOLogic.mk_tupleT o rev)
    4.44        in List.foldl (op -->) body_T batched end
    4.45    end
    4.46 -fun format_term_type thy def_table formats t =
    4.47 +fun format_term_type thy def_tables formats t =
    4.48    format_type (the (AList.lookup (op =) formats NONE))
    4.49 -              (lookup_format thy def_table formats t) (fastype_of t)
    4.50 +              (lookup_format thy def_tables formats t) (fastype_of t)
    4.51  
    4.52  fun repair_special_format js m format =
    4.53    m - 1 downto 0 |> chunk_list_unevenly (rev format)
    4.54                   |> map (rev o filter_out (member (op =) js))
    4.55                   |> filter_out null |> map length |> rev
    4.56  
    4.57 -fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
    4.58 +fun user_friendly_const ({thy, evals, def_tables, skolems, special_funs, ...}
    4.59                           : hol_context) (base_name, step_name) formats =
    4.60    let
    4.61      val default_format = the (AList.lookup (op =) formats NONE)
    4.62 @@ -762,7 +762,7 @@
    4.63                 SOME format =>
    4.64                 repair_special_format js (num_binder_types T') format
    4.65               | NONE =>
    4.66 -               const_format thy def_table x'
    4.67 +               const_format thy def_tables x'
    4.68                 |> repair_special_format js (num_binder_types T')
    4.69                 |> intersect_formats default_format
    4.70           in
    4.71 @@ -789,7 +789,7 @@
    4.72           let val t = Const (original_name s, range_type T) in
    4.73             (lambda (Free (iter_var_prefix, nat_T)) t,
    4.74              format_type default_format
    4.75 -                        (lookup_format thy def_table formats t) T)
    4.76 +                        (lookup_format thy def_tables formats t) T)
    4.77           end
    4.78         else if String.isPrefix base_prefix s then
    4.79           (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
    4.80 @@ -799,7 +799,7 @@
    4.81            format_type default_format default_format T)
    4.82         else if String.isPrefix quot_normal_prefix s then
    4.83           let val t = Const (nitpick_prefix ^ "quotient normal form", T) in
    4.84 -           (t, format_term_type thy def_table formats t)
    4.85 +           (t, format_term_type thy def_tables formats t)
    4.86           end
    4.87         else if String.isPrefix skolem_prefix s then
    4.88           let
    4.89 @@ -810,15 +810,15 @@
    4.90           in
    4.91             (fold lambda frees (Const (s', Ts' ---> T)),
    4.92              format_type default_format
    4.93 -                        (lookup_format thy def_table formats (Const x)) T)
    4.94 +                        (lookup_format thy def_tables formats (Const x)) T)
    4.95           end
    4.96         else if String.isPrefix eval_prefix s then
    4.97           let
    4.98             val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
    4.99 -         in (t, format_term_type thy def_table formats t) end
   4.100 +         in (t, format_term_type thy def_tables formats t) end
   4.101         else
   4.102           let val t = Const (original_name s, T) in
   4.103 -           (t, format_term_type thy def_table formats t)
   4.104 +           (t, format_term_type thy def_tables formats t)
   4.105           end)
   4.106        |>> map_types uniterize_unarize_unbox_etc_type
   4.107        |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   4.108 @@ -863,7 +863,7 @@
   4.109          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
   4.110                        debug, whacks, binary_ints, destroy_constrs, specialize,
   4.111                        star_linear_preds, tac_timeout, evals, case_names,
   4.112 -                      def_table, nondef_table, user_nondefs, simp_table,
   4.113 +                      def_tables, nondef_table, user_nondefs, simp_table,
   4.114                        psimp_table, choice_spec_table, intro_table,
   4.115                        ground_thm_table, ersatz_table, skolems, special_funs,
   4.116                        unrolled_preds, wf_cache, constr_cache},
   4.117 @@ -880,7 +880,7 @@
   4.118         whacks = whacks, binary_ints = binary_ints,
   4.119         destroy_constrs = destroy_constrs, specialize = specialize,
   4.120         star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
   4.121 -       evals = evals, case_names = case_names, def_table = def_table,
   4.122 +       evals = evals, case_names = case_names, def_tables = def_tables,
   4.123         nondef_table = nondef_table, user_nondefs = user_nondefs,
   4.124         simp_table = simp_table, psimp_table = psimp_table,
   4.125         choice_spec_table = choice_spec_table, intro_table = intro_table,
   4.126 @@ -912,7 +912,7 @@
   4.127            case name of
   4.128              FreeName (s, T, _) =>
   4.129              let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
   4.130 -              ("=", (t, format_term_type thy def_table formats t), T)
   4.131 +              ("=", (t, format_term_type thy def_tables formats t), T)
   4.132              end
   4.133            | ConstName (s, T, _) =>
   4.134              (assign_operator_for_const (s, T),
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 21 10:31:48 2011 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 21 10:42:29 2011 +0100
     5.3 @@ -540,7 +540,7 @@
     5.4  fun skolem_prefix_for k j =
     5.5    skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
     5.6  
     5.7 -fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
     5.8 +fun skolemize_term_and_more (hol_ctxt as {thy, def_tables, skolems, ...})
     5.9                              skolem_depth =
    5.10    let
    5.11      val incrs = map (Integer.add 1)
    5.12 @@ -615,7 +615,7 @@
    5.13               not (is_real_equational_fun hol_ctxt x) andalso
    5.14               not (is_well_founded_inductive_pred hol_ctxt x) then
    5.15              let
    5.16 -              val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
    5.17 +              val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
    5.18                val (pref, connective) =
    5.19                  if gfp then (lbfp_prefix, @{const HOL.disj})
    5.20                  else (ubfp_prefix, @{const HOL.conj})
    5.21 @@ -729,7 +729,7 @@
    5.22    forall (op aconv) (ts1 ~~ ts2)
    5.23  
    5.24  fun specialize_consts_in_term
    5.25 -        (hol_ctxt as {ctxt, thy, stds, specialize, def_table, simp_table,
    5.26 +        (hol_ctxt as {ctxt, thy, stds, specialize, def_tables, simp_table,
    5.27                        special_funs, ...}) def depth t =
    5.28    if not specialize orelse depth > special_max_depth then
    5.29      t
    5.30 @@ -742,7 +742,7 @@
    5.31                 not (String.isPrefix special_prefix s) andalso
    5.32                 not (is_built_in_const thy stds x) andalso
    5.33                 (is_equational_fun_but_no_plain_def hol_ctxt x orelse
    5.34 -                (is_some (def_of_const thy def_table x) andalso
    5.35 +                (is_some (def_of_const thy def_tables x) andalso
    5.36                   not (is_of_class_const thy x) andalso
    5.37                   not (is_constr ctxt stds x) andalso
    5.38                   not (is_choice_spec_fun hol_ctxt x))) then
    5.39 @@ -879,7 +879,8 @@
    5.40    | NONE => false
    5.41  
    5.42  fun all_table_entries table = Symtab.fold (append o snd) table []
    5.43 -fun extra_table table s = Symtab.make [(s, all_table_entries table)]
    5.44 +fun extra_table tables s =
    5.45 +  Symtab.make [(s, pairself all_table_entries tables |> op @)]
    5.46  
    5.47  fun eval_axiom_for_term j t =
    5.48    Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
    5.49 @@ -891,7 +892,7 @@
    5.50  
    5.51  fun axioms_for_term
    5.52          (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
    5.53 -                      evals, def_table, nondef_table, choice_spec_table,
    5.54 +                      evals, def_tables, nondef_table, choice_spec_table,
    5.55                        user_nondefs, ...}) assm_ts neg_t =
    5.56    let
    5.57      val (def_assm_ts, nondef_assm_ts) =
    5.58 @@ -962,7 +963,7 @@
    5.59                           range_type T = nat_T)
    5.60                          ? fold (add_maybe_def_axiom depth)
    5.61                                 (nondef_props_for_const thy true
    5.62 -                                                    (extra_table def_table s) x)
    5.63 +                                    (extra_table def_tables s) x)
    5.64               else if is_rep_fun ctxt x then
    5.65                 accum |> fold (add_nondef_axiom depth)
    5.66                               (nondef_props_for_const thy false nondef_table x)
    5.67 @@ -970,14 +971,14 @@
    5.68                           range_type T = nat_T)
    5.69                          ? fold (add_maybe_def_axiom depth)
    5.70                                 (nondef_props_for_const thy true
    5.71 -                                                    (extra_table def_table s) x)
    5.72 +                                    (extra_table def_tables s) x)
    5.73                       |> add_axioms_for_term depth
    5.74                                              (Const (mate_of_rep_fun ctxt x))
    5.75                       |> fold (add_def_axiom depth)
    5.76                               (inverse_axioms_for_rep_fun ctxt x)
    5.77               else if s = @{const_name TYPE} then
    5.78                 accum
    5.79 -             else case def_of_const thy def_table x of
    5.80 +             else case def_of_const thy def_tables x of
    5.81                 SOME _ =>
    5.82                 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
    5.83                      accum