--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 19 12:22:59 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 19 14:04:58 2011 +0200
@@ -270,14 +270,15 @@
val original_max_genuine = max_genuine
val max_bisim_depth = fold Integer.max bisim_depths ~1
val case_names = case_const_names ctxt stds
- val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
+ val defs = all_defs_of thy subst
+ val nondefs = all_nondefs_of ctxt subst
val def_tables = const_def_tables ctxt subst defs
- val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
+ val nondef_table = const_nondef_table nondefs
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
val psimp_table = const_psimp_table ctxt subst
val choice_spec_table = const_choice_spec_table ctxt subst
- val user_nondefs =
- user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
+ val nondefs =
+ nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
val intro_table = inductive_intro_table ctxt subst def_tables
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table ctxt
@@ -289,11 +290,11 @@
star_linear_preds = star_linear_preds, total_consts = total_consts,
needs = needs, tac_timeout = tac_timeout, evals = evals,
case_names = case_names, def_tables = def_tables,
- nondef_table = nondef_table, user_nondefs = user_nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
+ nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
+ special_funs = Unsynchronized.ref [],
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
val pseudo_frees = []