src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 41871 394eef237bd1
parent 41803 ef13e3b7cbaf
child 41875 e3cd0dce9b1a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 02 13:09:57 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 02 14:50:16 2011 +0100
     1.3 @@ -862,8 +862,8 @@
     1.4  fun reconstruct_hol_model {show_datatypes, show_consts}
     1.5          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
     1.6                        debug, whacks, binary_ints, destroy_constrs, specialize,
     1.7 -                      star_linear_preds, preconstrs, tac_timeout, evals,
     1.8 -                      case_names, def_tables, nondef_table, user_nondefs,
     1.9 +                      star_linear_preds, total_consts, preconstrs, tac_timeout,
    1.10 +                      evals, case_names, def_tables, nondef_table, user_nondefs,
    1.11                        simp_table, psimp_table, choice_spec_table, intro_table,
    1.12                        ground_thm_table, ersatz_table, skolems, special_funs,
    1.13                        unrolled_preds, wf_cache, constr_cache}, binarize,
    1.14 @@ -879,15 +879,16 @@
    1.15         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    1.16         whacks = whacks, binary_ints = binary_ints,
    1.17         destroy_constrs = destroy_constrs, specialize = specialize,
    1.18 -       star_linear_preds = star_linear_preds, preconstrs = preconstrs,
    1.19 -       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
    1.20 -       def_tables = def_tables, nondef_table = nondef_table,
    1.21 -       user_nondefs = user_nondefs, simp_table = simp_table,
    1.22 -       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    1.23 -       intro_table = intro_table, ground_thm_table = ground_thm_table,
    1.24 -       ersatz_table = ersatz_table, skolems = skolems,
    1.25 -       special_funs = special_funs, unrolled_preds = unrolled_preds,
    1.26 -       wf_cache = wf_cache, constr_cache = constr_cache}
    1.27 +       star_linear_preds = star_linear_preds, total_consts = total_consts,
    1.28 +       preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals,
    1.29 +       case_names = case_names, def_tables = def_tables,
    1.30 +       nondef_table = nondef_table, user_nondefs = user_nondefs,
    1.31 +       simp_table = simp_table, psimp_table = psimp_table,
    1.32 +       choice_spec_table = choice_spec_table, intro_table = intro_table,
    1.33 +       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    1.34 +       skolems = skolems, special_funs = special_funs,
    1.35 +       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
    1.36 +       constr_cache = constr_cache}
    1.37      val scope =
    1.38        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    1.39         bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}