36 val ersatz_table = ersatz_table ctxt |
36 val ersatz_table = ersatz_table ctxt |
37 val hol_ctxt as {thy, ...} : hol_context = |
37 val hol_ctxt as {thy, ...} : hol_context = |
38 {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [], |
38 {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [], |
39 stds = stds, wfs = [], user_axioms = NONE, debug = false, |
39 stds = stds, wfs = [], user_axioms = NONE, debug = false, |
40 whacks = [], binary_ints = SOME false, destroy_constrs = true, |
40 whacks = [], binary_ints = SOME false, destroy_constrs = true, |
41 specialize = false, star_linear_preds = false, preconstrs = [], |
41 specialize = false, star_linear_preds = false, total_consts = NONE, |
42 tac_timeout = NONE, evals = [], case_names = case_names, |
42 preconstrs = [], tac_timeout = NONE, evals = [], case_names = case_names, |
43 def_tables = def_tables, nondef_table = nondef_table, |
43 def_tables = def_tables, nondef_table = nondef_table, |
44 user_nondefs = user_nondefs, simp_table = simp_table, |
44 user_nondefs = user_nondefs, simp_table = simp_table, |
45 psimp_table = psimp_table, choice_spec_table = choice_spec_table, |
45 psimp_table = psimp_table, choice_spec_table = choice_spec_table, |
46 intro_table = intro_table, ground_thm_table = ground_thm_table, |
46 intro_table = intro_table, ground_thm_table = ground_thm_table, |
47 ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], |
47 ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], |