src/HOL/Nitpick_Examples/Mono_Nits.thy
changeset 42415 10accf397ab6
parent 41876 03f699556955
child 45035 60d2c03d5c70
     1.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Apr 19 12:22:59 2011 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Apr 19 14:04:58 2011 +0200
     1.3 @@ -23,14 +23,13 @@
     1.4  val stds = [(NONE, true)]
     1.5  val subst = []
     1.6  val case_names = case_const_names ctxt stds
     1.7 -val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
     1.8 +val defs = all_defs_of thy subst
     1.9 +val nondefs = all_nondefs_of ctxt subst
    1.10  val def_tables = const_def_tables ctxt subst defs
    1.11 -val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
    1.12 +val nondef_table = const_nondef_table nondefs
    1.13  val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
    1.14  val psimp_table = const_psimp_table ctxt subst
    1.15  val choice_spec_table = const_choice_spec_table ctxt subst
    1.16 -val user_nondefs =
    1.17 -  user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
    1.18  val intro_table = inductive_intro_table ctxt subst def_tables
    1.19  val ground_thm_table = ground_theorem_table thy
    1.20  val ersatz_table = ersatz_table ctxt
    1.21 @@ -40,13 +39,13 @@
    1.22     whacks = [], binary_ints = SOME false, destroy_constrs = true,
    1.23     specialize = false, star_linear_preds = false, total_consts = NONE,
    1.24     needs = NONE, tac_timeout = NONE, evals = [], case_names = case_names,
    1.25 -   def_tables = def_tables, nondef_table = nondef_table,
    1.26 -   user_nondefs = user_nondefs, simp_table = simp_table,
    1.27 -   psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    1.28 -   intro_table = intro_table, ground_thm_table = ground_thm_table,
    1.29 -   ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
    1.30 -   special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    1.31 -   wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
    1.32 +   def_tables = def_tables, nondef_table = nondef_table, nondefs = nondefs,
    1.33 +   simp_table = simp_table, psimp_table = psimp_table,
    1.34 +   choice_spec_table = choice_spec_table, intro_table = intro_table,
    1.35 +   ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    1.36 +   skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    1.37 +   unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    1.38 +   constr_cache = Unsynchronized.ref []}
    1.39  val binarize = false
    1.40  
    1.41  fun is_mono t =