860 end |
860 end |
861 |
861 |
862 fun reconstruct_hol_model {show_datatypes, show_consts} |
862 fun reconstruct_hol_model {show_datatypes, show_consts} |
863 ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms, |
863 ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms, |
864 debug, whacks, binary_ints, destroy_constrs, specialize, |
864 debug, whacks, binary_ints, destroy_constrs, specialize, |
865 star_linear_preds, total_consts, preconstrs, tac_timeout, |
865 star_linear_preds, total_consts, needs, tac_timeout, |
866 evals, case_names, def_tables, nondef_table, user_nondefs, |
866 evals, case_names, def_tables, nondef_table, user_nondefs, |
867 simp_table, psimp_table, choice_spec_table, intro_table, |
867 simp_table, psimp_table, choice_spec_table, intro_table, |
868 ground_thm_table, ersatz_table, skolems, special_funs, |
868 ground_thm_table, ersatz_table, skolems, special_funs, |
869 unrolled_preds, wf_cache, constr_cache}, binarize, |
869 unrolled_preds, wf_cache, constr_cache}, binarize, |
870 card_assigns, bits, bisim_depth, datatypes, ofs} : scope) |
870 card_assigns, bits, bisim_depth, datatypes, ofs} : scope) |
878 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, |
878 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, |
879 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, |
879 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, |
880 whacks = whacks, binary_ints = binary_ints, |
880 whacks = whacks, binary_ints = binary_ints, |
881 destroy_constrs = destroy_constrs, specialize = specialize, |
881 destroy_constrs = destroy_constrs, specialize = specialize, |
882 star_linear_preds = star_linear_preds, total_consts = total_consts, |
882 star_linear_preds = star_linear_preds, total_consts = total_consts, |
883 preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals, |
883 needs = needs, tac_timeout = tac_timeout, evals = evals, |
884 case_names = case_names, def_tables = def_tables, |
884 case_names = case_names, def_tables = def_tables, |
885 nondef_table = nondef_table, user_nondefs = user_nondefs, |
885 nondef_table = nondef_table, user_nondefs = user_nondefs, |
886 simp_table = simp_table, psimp_table = psimp_table, |
886 simp_table = simp_table, psimp_table = psimp_table, |
887 choice_spec_table = choice_spec_table, intro_table = intro_table, |
887 choice_spec_table = choice_spec_table, intro_table = intro_table, |
888 ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, |
888 ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, |