src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 33580 45c33e97cb86
parent 33571 3655e51f9958
child 33705 947184dc75c9
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Nov 05 17:00:28 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Nov 05 17:03:22 2009 +0100
     1.3 @@ -530,7 +530,7 @@
     1.4                         evals, case_names, def_table, nondef_table, user_nondefs,
     1.5                         simp_table, psimp_table, intro_table, ground_thm_table,
     1.6                         ersatz_table, skolems, special_funs, unrolled_preds,
     1.7 -                       wf_cache},
     1.8 +                       wf_cache, constr_cache},
     1.9           card_assigns, bisim_depth, datatypes, ofs} : scope) formats all_frees
    1.10          free_names sel_names nonsel_names rel_table bounds =
    1.11    let
    1.12 @@ -548,7 +548,7 @@
    1.13         intro_table = intro_table, ground_thm_table = ground_thm_table,
    1.14         ersatz_table = ersatz_table, skolems = skolems,
    1.15         special_funs = special_funs, unrolled_preds = unrolled_preds,
    1.16 -       wf_cache = wf_cache}
    1.17 +       wf_cache = wf_cache, constr_cache = constr_cache}
    1.18      val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
    1.19                   bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
    1.20      (* typ -> typ -> rep -> int list list -> term *)