--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 16:44:45 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 17:48:21 2010 +0200
@@ -843,11 +843,11 @@
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
debug, binary_ints, destroy_constrs, specialize,
- skolemize, star_linear_preds, uncurry, fast_descrs,
- tac_timeout, evals, case_names, def_table, 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},
+ skolemize, star_linear_preds, fast_descrs, tac_timeout,
+ evals, case_names, def_table, 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 all_frees free_names sel_names nonsel_names rel_table bounds =
let
@@ -859,19 +859,18 @@
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
binary_ints = binary_ints, destroy_constrs = destroy_constrs,
specialize = specialize, skolemize = skolemize,
- star_linear_preds = star_linear_preds, uncurry = uncurry,
- fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
- case_names = case_names, def_table = def_table,
- 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,
- unrolled_preds = unrolled_preds, wf_cache = wf_cache,
- constr_cache = constr_cache}
- val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
- card_assigns = card_assigns, bits = bits,
- bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
+ star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
+ tac_timeout = tac_timeout, evals = evals, case_names = case_names,
+ def_table = def_table, 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, unrolled_preds = unrolled_preds,
+ wf_cache = wf_cache, constr_cache = constr_cache}
+ val scope =
+ {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
+ bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
fun term_for_rep unfold =
reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
fun nth_value_of_type card T n =