src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 36389 8228b3a4a2ba
parent 36388 30f7ce76712d
child 36390 eee4ee6a5cbe
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Apr 24 17:48:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:10:30 2010 +0200
@@ -843,8 +843,8 @@
 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, fast_descrs, tac_timeout,
-                      evals, case_names, def_table, nondef_table, user_nondefs,
+                      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},
@@ -858,16 +858,16 @@
       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
        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, 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}
+       specialize = specialize, 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}