src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 36388 30f7ce76712d
parent 36385 ff5f88702590
child 36389 8228b3a4a2ba
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Apr 24 16:44:45 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Apr 24 17:48:21 2010 +0200
     1.3 @@ -843,11 +843,11 @@
     1.4  fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
     1.5          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
     1.6                        debug, binary_ints, destroy_constrs, specialize,
     1.7 -                      skolemize, star_linear_preds, uncurry, fast_descrs,
     1.8 -                      tac_timeout, evals, case_names, def_table, nondef_table,
     1.9 -                      user_nondefs, simp_table, psimp_table, choice_spec_table,
    1.10 -                      intro_table, ground_thm_table, ersatz_table, skolems,
    1.11 -                      special_funs, unrolled_preds, wf_cache, constr_cache},
    1.12 +                      skolemize, star_linear_preds, fast_descrs, tac_timeout,
    1.13 +                      evals, case_names, def_table, nondef_table, user_nondefs,
    1.14 +                      simp_table, psimp_table, choice_spec_table, intro_table,
    1.15 +                      ground_thm_table, ersatz_table, skolems, special_funs,
    1.16 +                      unrolled_preds, wf_cache, constr_cache},
    1.17           binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    1.18          formats all_frees free_names sel_names nonsel_names rel_table bounds =
    1.19    let
    1.20 @@ -859,19 +859,18 @@
    1.21         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    1.22         binary_ints = binary_ints, destroy_constrs = destroy_constrs,
    1.23         specialize = specialize, skolemize = skolemize,
    1.24 -       star_linear_preds = star_linear_preds, uncurry = uncurry,
    1.25 -       fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
    1.26 -       case_names = case_names, def_table = def_table,
    1.27 -       nondef_table = nondef_table, user_nondefs = user_nondefs,
    1.28 -       simp_table = simp_table, psimp_table = psimp_table,
    1.29 -       choice_spec_table = choice_spec_table, intro_table = intro_table,
    1.30 -       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    1.31 -       skolems = skolems, special_funs = special_funs,
    1.32 -       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
    1.33 -       constr_cache = constr_cache}
    1.34 -    val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
    1.35 -                 card_assigns = card_assigns, bits = bits,
    1.36 -                 bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
    1.37 +       star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
    1.38 +       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
    1.39 +       def_table = def_table, nondef_table = nondef_table,
    1.40 +       user_nondefs = user_nondefs, simp_table = simp_table,
    1.41 +       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    1.42 +       intro_table = intro_table, ground_thm_table = ground_thm_table,
    1.43 +       ersatz_table = ersatz_table, skolems = skolems,
    1.44 +       special_funs = special_funs, unrolled_preds = unrolled_preds,
    1.45 +       wf_cache = wf_cache, constr_cache = constr_cache}
    1.46 +    val scope =
    1.47 +      {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    1.48 +       bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
    1.49      fun term_for_rep unfold =
    1.50        reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
    1.51      fun nth_value_of_type card T n =