src/HOL/Tools/Nitpick/nitpick.ML
changeset 42415 10accf397ab6
parent 42361 23f352990944
child 42486 01b03a124b81
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 19 12:22:59 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 19 14:04:58 2011 +0200
     1.3 @@ -270,14 +270,15 @@
     1.4      val original_max_genuine = max_genuine
     1.5      val max_bisim_depth = fold Integer.max bisim_depths ~1
     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 nondefs =
    1.19 +      nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
    1.20      val intro_table = inductive_intro_table ctxt subst def_tables
    1.21      val ground_thm_table = ground_theorem_table thy
    1.22      val ersatz_table = ersatz_table ctxt
    1.23 @@ -289,11 +290,11 @@
    1.24         star_linear_preds = star_linear_preds, total_consts = total_consts,
    1.25         needs = needs, tac_timeout = tac_timeout, evals = evals,
    1.26         case_names = case_names, def_tables = def_tables,
    1.27 -       nondef_table = nondef_table, user_nondefs = user_nondefs,
    1.28 -       simp_table = simp_table, psimp_table = psimp_table,
    1.29 -       choice_spec_table = choice_spec_table, intro_table = intro_table,
    1.30 -       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    1.31 -       skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    1.32 +       nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
    1.33 +       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    1.34 +       intro_table = intro_table, ground_thm_table = ground_thm_table,
    1.35 +       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
    1.36 +       special_funs = Unsynchronized.ref [],
    1.37         unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    1.38         constr_cache = Unsynchronized.ref []}
    1.39      val pseudo_frees = []