use "Spec_Rules" for finding axioms -- more reliable and cleaner
authorblanchet
Tue Apr 19 14:04:58 2011 +0200 (2011-04-19)
changeset 4241510accf397ab6
parent 42414 9465651c0db7
child 42417 574393cb3d9d
child 42418 508acf776ebf
use "Spec_Rules" for finding axioms -- more reliable and cleaner
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Tue Apr 19 12:22:59 2011 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,108 +0,0 @@
     1.4 -(*  Title:      HOL/Nitpick_Examples/Mini_Nits.thy
     1.5 -    Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2009, 2010
     1.7 -
     1.8 -Examples featuring Minipick, the minimalistic version of Nitpick.
     1.9 -*)
    1.10 -
    1.11 -header {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}
    1.12 -
    1.13 -theory Mini_Nits
    1.14 -imports Main
    1.15 -begin
    1.16 -
    1.17 -ML {*
    1.18 -exception FAIL
    1.19 -
    1.20 -val has_kodkodi = (getenv "KODKODI" <> "")
    1.21 -
    1.22 -fun minipick n t =
    1.23 -  map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
    1.24 -  |> Minipick.solve_any_kodkod_problem @{theory}
    1.25 -fun minipick_expect expect n t =
    1.26 -  if has_kodkodi then
    1.27 -    if minipick n t = expect then () else raise FAIL
    1.28 -  else
    1.29 -    ()
    1.30 -val none = minipick_expect "none"
    1.31 -val genuine = minipick_expect "genuine"
    1.32 -val unknown = minipick_expect "unknown"
    1.33 -*}
    1.34 -
    1.35 -ML {* genuine 1 @{prop "x = Not"} *}
    1.36 -ML {* none 1 @{prop "\<exists>x. x = Not"} *}
    1.37 -ML {* none 1 @{prop "\<not> False"} *}
    1.38 -ML {* genuine 1 @{prop "\<not> True"} *}
    1.39 -ML {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
    1.40 -ML {* none 1 @{prop True} *}
    1.41 -ML {* genuine 1 @{prop False} *}
    1.42 -ML {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
    1.43 -ML {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
    1.44 -ML {* none 5 @{prop "\<forall>x. x = x"} *}
    1.45 -ML {* none 5 @{prop "\<exists>x. x = x"} *}
    1.46 -ML {* none 1 @{prop "\<forall>x. x = y"} *}
    1.47 -ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
    1.48 -ML {* none 1 @{prop "\<exists>x. x = y"} *}
    1.49 -ML {* none 2 @{prop "\<exists>x. x = y"} *}
    1.50 -ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
    1.51 -ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
    1.52 -ML {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
    1.53 -ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
    1.54 -ML {* none 1 @{prop "All = Ex"} *}
    1.55 -ML {* genuine 2 @{prop "All = Ex"} *}
    1.56 -ML {* none 1 @{prop "All P = Ex P"} *}
    1.57 -ML {* genuine 2 @{prop "All P = Ex P"} *}
    1.58 -ML {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
    1.59 -ML {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
    1.60 -ML {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
    1.61 -ML {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
    1.62 -ML {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
    1.63 -ML {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
    1.64 -ML {* genuine 1 @{prop "(op =) X = Ex"} *}
    1.65 -ML {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
    1.66 -ML {* none 1 @{prop "x = y"} *}
    1.67 -ML {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
    1.68 -ML {* genuine 2 @{prop "x = y"} *}
    1.69 -ML {* genuine 1 @{prop "X \<subseteq> Y"} *}
    1.70 -ML {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
    1.71 -ML {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
    1.72 -ML {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
    1.73 -ML {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
    1.74 -ML {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
    1.75 -ML {* none 5 @{prop "{a} = {a, a}"} *}
    1.76 -ML {* genuine 2 @{prop "{a} = {a, b}"} *}
    1.77 -ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
    1.78 -ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
    1.79 -ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.80 -ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.81 -ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.82 -ML {* none 5 @{prop "A \<union> B = (\<lambda>x. A x \<or> B x)"} *}
    1.83 -ML {* none 5 @{prop "A \<inter> B = (\<lambda>x. A x \<and> B x)"} *}
    1.84 -ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
    1.85 -ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
    1.86 -ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
    1.87 -ML {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
    1.88 -ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
    1.89 -ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
    1.90 -ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
    1.91 -ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
    1.92 -ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
    1.93 -ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
    1.94 -ML {* none 5 @{prop "fst (a, b) = a"} *}
    1.95 -ML {* none 1 @{prop "fst (a, b) = b"} *}
    1.96 -ML {* genuine 2 @{prop "fst (a, b) = b"} *}
    1.97 -ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
    1.98 -ML {* none 5 @{prop "snd (a, b) = b"} *}
    1.99 -ML {* none 1 @{prop "snd (a, b) = a"} *}
   1.100 -ML {* genuine 2 @{prop "snd (a, b) = a"} *}
   1.101 -ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
   1.102 -ML {* genuine 1 @{prop P} *}
   1.103 -ML {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
   1.104 -ML {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
   1.105 -ML {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
   1.106 -ML {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
   1.107 -ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
   1.108 -ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
   1.109 -ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
   1.110 -
   1.111 -end
     2.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Apr 19 12:22:59 2011 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Apr 19 14:04:58 2011 +0200
     2.3 @@ -23,14 +23,13 @@
     2.4  val stds = [(NONE, true)]
     2.5  val subst = []
     2.6  val case_names = case_const_names ctxt stds
     2.7 -val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
     2.8 +val defs = all_defs_of thy subst
     2.9 +val nondefs = all_nondefs_of ctxt subst
    2.10  val def_tables = const_def_tables ctxt subst defs
    2.11 -val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
    2.12 +val nondef_table = const_nondef_table nondefs
    2.13  val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
    2.14  val psimp_table = const_psimp_table ctxt subst
    2.15  val choice_spec_table = const_choice_spec_table ctxt subst
    2.16 -val user_nondefs =
    2.17 -  user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
    2.18  val intro_table = inductive_intro_table ctxt subst def_tables
    2.19  val ground_thm_table = ground_theorem_table thy
    2.20  val ersatz_table = ersatz_table ctxt
    2.21 @@ -40,13 +39,13 @@
    2.22     whacks = [], binary_ints = SOME false, destroy_constrs = true,
    2.23     specialize = false, star_linear_preds = false, total_consts = NONE,
    2.24     needs = NONE, tac_timeout = NONE, evals = [], case_names = case_names,
    2.25 -   def_tables = def_tables, nondef_table = nondef_table,
    2.26 -   user_nondefs = user_nondefs, simp_table = simp_table,
    2.27 -   psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    2.28 -   intro_table = intro_table, ground_thm_table = ground_thm_table,
    2.29 -   ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
    2.30 -   special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    2.31 -   wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
    2.32 +   def_tables = def_tables, nondef_table = nondef_table, nondefs = nondefs,
    2.33 +   simp_table = simp_table, psimp_table = psimp_table,
    2.34 +   choice_spec_table = choice_spec_table, intro_table = intro_table,
    2.35 +   ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    2.36 +   skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    2.37 +   unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    2.38 +   constr_cache = Unsynchronized.ref []}
    2.39  val binarize = false
    2.40  
    2.41  fun is_mono t =
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 19 12:22:59 2011 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 19 14:04:58 2011 +0200
     3.3 @@ -270,14 +270,15 @@
     3.4      val original_max_genuine = max_genuine
     3.5      val max_bisim_depth = fold Integer.max bisim_depths ~1
     3.6      val case_names = case_const_names ctxt stds
     3.7 -    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
     3.8 +    val defs = all_defs_of thy subst
     3.9 +    val nondefs = all_nondefs_of ctxt subst
    3.10      val def_tables = const_def_tables ctxt subst defs
    3.11 -    val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
    3.12 +    val nondef_table = const_nondef_table nondefs
    3.13      val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
    3.14      val psimp_table = const_psimp_table ctxt subst
    3.15      val choice_spec_table = const_choice_spec_table ctxt subst
    3.16 -    val user_nondefs =
    3.17 -      user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
    3.18 +    val nondefs =
    3.19 +      nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
    3.20      val intro_table = inductive_intro_table ctxt subst def_tables
    3.21      val ground_thm_table = ground_theorem_table thy
    3.22      val ersatz_table = ersatz_table ctxt
    3.23 @@ -289,11 +290,11 @@
    3.24         star_linear_preds = star_linear_preds, total_consts = total_consts,
    3.25         needs = needs, tac_timeout = tac_timeout, evals = evals,
    3.26         case_names = case_names, def_tables = def_tables,
    3.27 -       nondef_table = nondef_table, user_nondefs = user_nondefs,
    3.28 -       simp_table = simp_table, psimp_table = psimp_table,
    3.29 -       choice_spec_table = choice_spec_table, intro_table = intro_table,
    3.30 -       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    3.31 -       skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    3.32 +       nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
    3.33 +       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    3.34 +       intro_table = intro_table, ground_thm_table = ground_thm_table,
    3.35 +       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
    3.36 +       special_funs = Unsynchronized.ref [],
    3.37         unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    3.38         constr_cache = Unsynchronized.ref []}
    3.39      val pseudo_frees = []
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 12:22:59 2011 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 14:04:58 2011 +0200
     4.3 @@ -34,7 +34,7 @@
     4.4       case_names: (string * int) list,
     4.5       def_tables: const_table * const_table,
     4.6       nondef_table: const_table,
     4.7 -     user_nondefs: term list,
     4.8 +     nondefs: term list,
     4.9       simp_table: const_table Unsynchronized.ref,
    4.10       psimp_table: const_table,
    4.11       choice_spec_table: const_table,
    4.12 @@ -181,8 +181,8 @@
    4.13    val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
    4.14    val special_bounds : term list -> (indexname * typ) list
    4.15    val is_funky_typedef : Proof.context -> typ -> bool
    4.16 -  val all_axioms_of :
    4.17 -    Proof.context -> (term * term) list -> term list * term list * term list
    4.18 +  val all_defs_of : theory -> (term * term) list -> term list
    4.19 +  val all_nondefs_of : Proof.context -> (term * term) list -> term list
    4.20    val arity_of_built_in_const :
    4.21      theory -> (typ option * bool) list -> styp -> int option
    4.22    val is_built_in_const :
    4.23 @@ -267,7 +267,7 @@
    4.24     case_names: (string * int) list,
    4.25     def_tables: const_table * const_table,
    4.26     nondef_table: const_table,
    4.27 -   user_nondefs: term list,
    4.28 +   nondefs: term list,
    4.29     simp_table: const_table Unsynchronized.ref,
    4.30     psimp_table: const_table,
    4.31     choice_spec_table: const_table,
    4.32 @@ -1255,9 +1255,6 @@
    4.33    is_frac_type ctxt (Type (s, []))
    4.34  fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
    4.35    | is_funky_typedef _ _ = false
    4.36 -fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
    4.37 -                         $ Const (@{const_name TYPE}, _)) = true
    4.38 -  | is_arity_type_axiom _ = false
    4.39  fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
    4.40      is_typedef_axiom ctxt boring t2
    4.41    | is_typedef_axiom ctxt boring
    4.42 @@ -1266,21 +1263,15 @@
    4.43           $ Const _ $ _)) =
    4.44      boring <> is_funky_typedef_name ctxt s andalso is_typedef ctxt s
    4.45    | is_typedef_axiom _ _ _ = false
    4.46 -val is_class_axiom =
    4.47 -  Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
    4.48  
    4.49  (* Distinguishes between (1) constant definition axioms, (2) type arity and
    4.50     typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
    4.51     Typedef axioms are uninteresting to Nitpick, because it can retrieve them
    4.52     using "typedef_info". *)
    4.53 -fun partition_axioms_by_definitionality ctxt axioms def_names =
    4.54 -  let
    4.55 -    val axioms = sort (fast_string_ord o pairself fst) axioms
    4.56 -    val defs = Ord_List.inter (fast_string_ord o apsnd fst) def_names axioms
    4.57 -    val nondefs =
    4.58 -      Ord_List.subtract (fast_string_ord o apsnd fst) def_names axioms
    4.59 -      |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
    4.60 -  in pairself (map snd) (defs, nondefs) end
    4.61 +fun filter_defs def_names =
    4.62 +  sort (fast_string_ord o pairself fst)
    4.63 +  #> Ord_List.inter (fast_string_ord o apsnd fst) def_names
    4.64 +  #> map snd
    4.65  
    4.66  (* Ideally we would check against "Complex_Main", not "Refute", but any theory
    4.67     will do as long as it contains all the "axioms" and "axiomatization"
    4.68 @@ -1302,36 +1293,32 @@
    4.69        | do_eq _ = false
    4.70    in do_eq end
    4.71  
    4.72 -fun all_axioms_of ctxt subst =
    4.73 +fun all_defs_of thy subst =
    4.74    let
    4.75 -    val thy = Proof_Context.theory_of ctxt
    4.76 -    val axioms_of_thys =
    4.77 -      maps Thm.axioms_of
    4.78 -      #> map (apsnd (subst_atomic subst o prop_of))
    4.79 -      #> filter_out (is_class_axiom o snd)
    4.80 -    val specs = Defs.all_specifications_of (Theory.defs_of thy)
    4.81 -    val def_names = specs |> maps snd |> map_filter #def
    4.82 -                    |> Ord_List.make fast_string_ord
    4.83 +    val def_names =
    4.84 +      thy |> Theory.defs_of
    4.85 +          |> Defs.all_specifications_of
    4.86 +          |> maps snd |> map_filter #def
    4.87 +          |> Ord_List.make fast_string_ord
    4.88      val thys = thy :: Theory.ancestors_of thy
    4.89 -    val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
    4.90 -    val built_in_axioms = axioms_of_thys built_in_thys
    4.91 -    val user_axioms = axioms_of_thys user_thys
    4.92 -    val (built_in_defs, built_in_nondefs) =
    4.93 -      partition_axioms_by_definitionality ctxt built_in_axioms def_names
    4.94 -      ||> filter (is_typedef_axiom ctxt false)
    4.95 -    val (user_defs, user_nondefs) =
    4.96 -      partition_axioms_by_definitionality ctxt user_axioms def_names
    4.97 -    val (built_in_nondefs, user_nondefs) =
    4.98 -      List.partition (is_typedef_axiom ctxt false) user_nondefs
    4.99 -      |>> append built_in_nondefs
   4.100 -    val defs =
   4.101 -      (thy |> Global_Theory.all_thms_of
   4.102 -           |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
   4.103 -           |> map (prop_of o snd)
   4.104 -           |> filter_out is_trivial_definition
   4.105 -           |> filter is_plain_definition) @
   4.106 -      user_defs @ built_in_defs
   4.107 -  in (defs, built_in_nondefs, user_nondefs) end
   4.108 +  in
   4.109 +    (* FIXME: avoid relying on "Thm.definitionK" *)
   4.110 +    (thy |> Global_Theory.all_thms_of
   4.111 +         |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
   4.112 +         |> map (subst_atomic subst o prop_of o snd)
   4.113 +         |> filter_out is_trivial_definition
   4.114 +         |> filter is_plain_definition) @
   4.115 +    (thys |> maps Thm.axioms_of
   4.116 +          |> map (apsnd (subst_atomic subst o prop_of))
   4.117 +          |> filter_defs def_names)
   4.118 +  end
   4.119 +
   4.120 +fun all_nondefs_of ctxt subst =
   4.121 +  ctxt |> Spec_Rules.get
   4.122 +       |> filter (curry (op =) Spec_Rules.Unknown o fst)
   4.123 +       |> maps (snd o snd)
   4.124 +       |> filter_out (is_built_in_theory o theory_of_thm)
   4.125 +       |> map (subst_atomic subst o prop_of)
   4.126  
   4.127  fun arity_of_built_in_const thy stds (s, T) =
   4.128    if s = @{const_name If} then
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Apr 19 12:22:59 2011 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Apr 19 14:04:58 2011 +0200
     5.3 @@ -865,7 +865,7 @@
     5.4          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
     5.5                        debug, whacks, binary_ints, destroy_constrs, specialize,
     5.6                        star_linear_preds, total_consts, needs, tac_timeout,
     5.7 -                      evals, case_names, def_tables, nondef_table, user_nondefs,
     5.8 +                      evals, case_names, def_tables, nondef_table, nondefs,
     5.9                        simp_table, psimp_table, choice_spec_table, intro_table,
    5.10                        ground_thm_table, ersatz_table, skolems, special_funs,
    5.11                        unrolled_preds, wf_cache, constr_cache}, binarize,
    5.12 @@ -884,13 +884,12 @@
    5.13         star_linear_preds = star_linear_preds, total_consts = total_consts,
    5.14         needs = needs, tac_timeout = tac_timeout, evals = evals,
    5.15         case_names = case_names, def_tables = def_tables,
    5.16 -       nondef_table = nondef_table, user_nondefs = user_nondefs,
    5.17 -       simp_table = simp_table, psimp_table = psimp_table,
    5.18 -       choice_spec_table = choice_spec_table, intro_table = intro_table,
    5.19 -       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    5.20 -       skolems = skolems, special_funs = special_funs,
    5.21 -       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
    5.22 -       constr_cache = constr_cache}
    5.23 +       nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
    5.24 +       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    5.25 +       intro_table = intro_table, ground_thm_table = ground_thm_table,
    5.26 +       ersatz_table = ersatz_table, skolems = skolems,
    5.27 +       special_funs = special_funs, unrolled_preds = unrolled_preds,
    5.28 +       wf_cache = wf_cache, constr_cache = constr_cache}
    5.29      val scope =
    5.30        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    5.31         bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Apr 19 12:22:59 2011 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Apr 19 14:04:58 2011 +0200
     6.3 @@ -889,7 +889,7 @@
     6.4  fun axioms_for_term
     6.5          (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
     6.6                        evals, def_tables, nondef_table, choice_spec_table,
     6.7 -                      user_nondefs, ...}) assm_ts neg_t =
     6.8 +                      nondefs, ...}) assm_ts neg_t =
     6.9    let
    6.10      val (def_assm_ts, nondef_assm_ts) =
    6.11        List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
    6.12 @@ -1030,8 +1030,8 @@
    6.13                                            \add_axioms_for_sort", [t]))
    6.14                class_axioms
    6.15        in fold (add_nondef_axiom depth) monomorphic_class_axioms end
    6.16 -    val (mono_user_nondefs, poly_user_nondefs) =
    6.17 -      List.partition (null o Term.hidden_polymorphism) user_nondefs
    6.18 +    val (mono_nondefs, poly_nondefs) =
    6.19 +      List.partition (null o Term.hidden_polymorphism) nondefs
    6.20      val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
    6.21                             evals
    6.22      val (seen, (defs, nondefs)) =
    6.23 @@ -1039,13 +1039,11 @@
    6.24        |> add_axioms_for_term 1 neg_t
    6.25        |> fold_rev (add_nondef_axiom 1) nondef_assm_ts
    6.26        |> fold_rev (add_def_axiom 1) eval_axioms
    6.27 -      |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_user_nondefs
    6.28 +      |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_nondefs
    6.29      val defs = defs @ special_congruence_axioms hol_ctxt seen
    6.30      val got_all_mono_user_axioms =
    6.31 -      (user_axioms = SOME true orelse null mono_user_nondefs)
    6.32 -  in
    6.33 -    (neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs)
    6.34 -  end
    6.35 +      (user_axioms = SOME true orelse null mono_nondefs)
    6.36 +  in (neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_nondefs) end
    6.37  
    6.38  (** Simplification of constructor/selector terms **)
    6.39