src/HOL/Tools/Nitpick/nitpick_model.ML

   | dest_n_tuple_type n (Type (_, [T1, T2])) =
     T1 :: dest_n_tuple_type (n - 1) T2
   | dest_n_tuple_type _ T =
     raise TYPE ("Nitpick_Model.dest_n_tuple_type", [T], [])
 
-fun const_format thy def_table (x as (s, T)) =
+fun const_format thy def_tables (x as (s, T)) =
   if String.isPrefix unrolled_prefix s then
-    const_format thy def_table (original_name s, range_type T)
+    const_format thy def_tables (original_name s, range_type T)
   else if String.isPrefix skolem_prefix s then
     let
       val k = unprefix skolem_prefix s
               |> strip_first_name_sep |> fst |> space_explode "@"
               |> hd |> Int.fromString |> the
     in [k, num_binder_types T - k] end
   else if original_name s <> s then
     [num_binder_types T]
-  else case def_of_const thy def_table x of
+  else case def_of_const thy def_tables x of
     SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
                  let val k = length (strip_abs_vars t') in
                    [k, num_binder_types T - k]
                  end
                else

       intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
                         (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
       [Int.min (k1, k2)]
     end
 
-fun lookup_format thy def_table formats t =
+fun lookup_format thy def_tables formats t =
   case AList.lookup (fn (SOME x, SOME y) =>
                         (term_match thy) (x, y) | _ => false)
                     formats (SOME t) of
     SOME format => format
   | NONE => let val format = the (AList.lookup (op =) formats NONE) in
               case t of
                 Const x => intersect_formats format
-                                             (const_format thy def_table x)
+                                             (const_format thy def_tables x)
               | _ => format
             end
 
 fun format_type default_format format T =
   let

           |> map (format_type default_format default_format)
           |> rev |> chunk_list_unevenly (rev format)
           |> map (HOLogic.mk_tupleT o rev)
       in List.foldl (op -->) body_T batched end
   end
-fun format_term_type thy def_table formats t =
+fun format_term_type thy def_tables formats t =
   format_type (the (AList.lookup (op =) formats NONE))
-              (lookup_format thy def_table formats t) (fastype_of t)
+              (lookup_format thy def_tables formats t) (fastype_of t)
 
 fun repair_special_format js m format =
   m - 1 downto 0 |> chunk_list_unevenly (rev format)
                  |> map (rev o filter_out (member (op =) js))
                  |> filter_out null |> map length |> rev
 
-fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
+fun user_friendly_const ({thy, evals, def_tables, skolems, special_funs, ...}
                          : hol_context) (base_name, step_name) formats =
   let
     val default_format = the (AList.lookup (op =) formats NONE)
     fun do_const (x as (s, T)) =
       (if String.isPrefix special_prefix s then

              case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
                                  | _ => false) formats (SOME t) of
                SOME format =>
                repair_special_format js (num_binder_types T') format
              | NONE =>
-               const_format thy def_table x'
+               const_format thy def_tables x'
                |> repair_special_format js (num_binder_types T')
                |> intersect_formats default_format
          in
            (list_comb (t, ts') |> fold_rev abs_var vars,
             format_type default_format format T)

          end
        else if String.isPrefix unrolled_prefix s then
          let val t = Const (original_name s, range_type T) in
            (lambda (Free (iter_var_prefix, nat_T)) t,
             format_type default_format
-                        (lookup_format thy def_table formats t) T)
+                        (lookup_format thy def_tables formats t) T)
          end
        else if String.isPrefix base_prefix s then
          (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
           format_type default_format default_format T)
        else if String.isPrefix step_prefix s then
          (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
           format_type default_format default_format T)
        else if String.isPrefix quot_normal_prefix s then
          let val t = Const (nitpick_prefix ^ "quotient normal form", T) in
-           (t, format_term_type thy def_table formats t)
+           (t, format_term_type thy def_tables formats t)
          end
        else if String.isPrefix skolem_prefix s then
          let
            val ss = the (AList.lookup (op =) (!skolems) s)
            val (Ts, Ts') = chop (length ss) (binder_types T)
            val frees = map Free (ss ~~ Ts)
            val s' = original_name s
          in
            (fold lambda frees (Const (s', Ts' ---> T)),
             format_type default_format
-                        (lookup_format thy def_table formats (Const x)) T)
+                        (lookup_format thy def_tables formats (Const x)) T)
          end
        else if String.isPrefix eval_prefix s then
          let
            val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
-         in (t, format_term_type thy def_table formats t) end
+         in (t, format_term_type thy def_tables formats t) end
        else
          let val t = Const (original_name s, T) in
-           (t, format_term_type thy def_table formats t)
+           (t, format_term_type thy def_tables formats t)
          end)
       |>> map_types uniterize_unarize_unbox_etc_type
       |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   in do_const end
 

 
 fun reconstruct_hol_model {show_datatypes, show_consts}
         ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
                       debug, whacks, binary_ints, destroy_constrs, specialize,
                       star_linear_preds, tac_timeout, evals, case_names,
-                      def_table, nondef_table, user_nondefs, simp_table,
+                      def_tables, nondef_table, user_nondefs, simp_table,
                       psimp_table, choice_spec_table, intro_table,
                       ground_thm_table, ersatz_table, skolems, special_funs,
                       unrolled_preds, wf_cache, constr_cache},
          binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
         formats atomss real_frees pseudo_frees free_names sel_names nonsel_names

       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
        stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
        whacks = whacks, binary_ints = binary_ints,
        destroy_constrs = destroy_constrs, specialize = specialize,
        star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
-       evals = evals, case_names = case_names, def_table = def_table,
+       evals = evals, case_names = case_names, def_tables = def_tables,
        nondef_table = nondef_table, user_nondefs = user_nondefs,
        simp_table = simp_table, psimp_table = psimp_table,
        choice_spec_table = choice_spec_table, intro_table = intro_table,
        ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
        skolems = skolems, special_funs = special_funs,

       let
         val (oper, (t1, T'), T) =
           case name of
             FreeName (s, T, _) =>
             let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
-              ("=", (t, format_term_type thy def_table formats t), T)
+              ("=", (t, format_term_type thy def_tables formats t), T)
             end
           | ConstName (s, T, _) =>
             (assign_operator_for_const (s, T),
              user_friendly_const hol_ctxt base_step_names formats (s, T), T)
           | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\