32 val user_nondefs = |
32 val user_nondefs = |
33 user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table) |
33 user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table) |
34 val intro_table = inductive_intro_table ctxt subst def_table |
34 val intro_table = inductive_intro_table ctxt subst def_table |
35 val ground_thm_table = ground_theorem_table thy |
35 val ground_thm_table = ground_theorem_table thy |
36 val ersatz_table = ersatz_table ctxt |
36 val ersatz_table = ersatz_table ctxt |
37 val hol_ctxt as {thy, ...} = |
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, |
41 specialize = false, star_linear_preds = false, |
42 tac_timeout = NONE, evals = [], case_names = case_names, |
42 tac_timeout = NONE, evals = [], case_names = case_names, |