src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35807 e4d1b5cbd429
parent 35718 eee1a5e0d334
child 35845 e5980f0ad025
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Mar 16 08:45:08 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 17 09:14:43 2010 +0100
     1.3 @@ -917,9 +917,9 @@
     1.4                        debug, binary_ints, destroy_constrs, specialize,
     1.5                        skolemize, star_linear_preds, uncurry, fast_descrs,
     1.6                        tac_timeout, evals, case_names, def_table, nondef_table,
     1.7 -                      user_nondefs, simp_table, psimp_table, intro_table,
     1.8 -                      ground_thm_table, ersatz_table, skolems, special_funs,
     1.9 -                      unrolled_preds, wf_cache, constr_cache},
    1.10 +                      user_nondefs, simp_table, psimp_table, choice_spec_table,
    1.11 +                      intro_table, ground_thm_table, ersatz_table, skolems,
    1.12 +                      special_funs, unrolled_preds, wf_cache, constr_cache},
    1.13           binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    1.14          formats all_frees free_names sel_names nonsel_names rel_table bounds =
    1.15    let
    1.16 @@ -936,10 +936,11 @@
    1.17         case_names = case_names, def_table = def_table,
    1.18         nondef_table = nondef_table, user_nondefs = user_nondefs,
    1.19         simp_table = simp_table, psimp_table = psimp_table,
    1.20 -       intro_table = intro_table, ground_thm_table = ground_thm_table,
    1.21 -       ersatz_table = ersatz_table, skolems = skolems,
    1.22 -       special_funs = special_funs, unrolled_preds = unrolled_preds,
    1.23 -       wf_cache = wf_cache, constr_cache = constr_cache}
    1.24 +       choice_spec_table = choice_spec_table, intro_table = intro_table,
    1.25 +       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    1.26 +       skolems = skolems, special_funs = special_funs,
    1.27 +       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
    1.28 +       constr_cache = constr_cache}
    1.29      val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
    1.30                   card_assigns = card_assigns, bits = bits,
    1.31                   bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}