removed nonstandard models from Nitpick
authorblanchet
Mon Mar 03 22:33:22 2014 +0100 (2014-03-03)
changeset 55888cac1add157e8
parent 55887 25bd4745ee38
child 55889 6bfbec3dff62
removed nonstandard models from Nitpick
src/Doc/Nitpick/document/root.tex
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/Doc/Nitpick/document/root.tex	Mon Mar 03 16:44:46 2014 +0100
     1.2 +++ b/src/Doc/Nitpick/document/root.tex	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -1384,121 +1384,6 @@
     1.4  
     1.5  and this time \textit{arith} can finish off the subgoals.
     1.6  
     1.7 -A similar technique can be employed for structural induction. The
     1.8 -following mini formalization of full binary trees will serve as illustration:
     1.9 -
    1.10 -\prew
    1.11 -\textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
    1.12 -\textbf{primrec}~\textit{labels}~\textbf{where} \\
    1.13 -``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\mid$ \\
    1.14 -``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[2\smallskipamount]
    1.15 -\textbf{primrec}~\textit{swap}~\textbf{where} \\
    1.16 -``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\
    1.17 -\phantom{``}$(\textrm{if}~c = a~\textrm{then}~\textit{Leaf}~b~\textrm{else~if}~c = b~\textrm{then}~\textit{Leaf}~a~\textrm{else}~\textit{Leaf}~c)$'' $\mid$ \\
    1.18 -``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$''
    1.19 -\postw
    1.20 -
    1.21 -The \textit{labels} function returns the set of labels occurring on leaves of a
    1.22 -tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct
    1.23 -labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree
    1.24 -obtained by swapping $a$ and $b$:
    1.25 -
    1.26 -\prew
    1.27 -\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
    1.28 -\postw
    1.29 -
    1.30 -Nitpick can't find any counterexample, so we proceed with induction
    1.31 -(this time favoring a more structured style):
    1.32 -
    1.33 -\prew
    1.34 -\textbf{proof}~(\textit{induct}~$t$) \\
    1.35 -\hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\
    1.36 -\textbf{next} \\
    1.37 -\hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case}
    1.38 -\postw
    1.39 -
    1.40 -Nitpick can't find any counterexample at this point either, but it makes the
    1.41 -following suggestion:
    1.42 -
    1.43 -\prew
    1.44 -\slshape
    1.45 -Hint: To check that the induction hypothesis is general enough, try this command:
    1.46 -\textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
    1.47 -\postw
    1.48 -
    1.49 -If we follow the hint, we get a ``nonstandard'' counterexample for the step:
    1.50 -
    1.51 -\prew
    1.52 -\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
    1.53 -\hbox{}\qquad Free variables: \nopagebreak \\
    1.54 -\hbox{}\qquad\qquad $a = a_1$ \\
    1.55 -\hbox{}\qquad\qquad $b = a_2$ \\
    1.56 -\hbox{}\qquad\qquad $t = \xi_1$ \\
    1.57 -\hbox{}\qquad\qquad $u = \xi_2$ \\
    1.58 -\hbox{}\qquad Datatype: \nopagebreak \\
    1.59 -\hbox{}\qquad\qquad $'a~\textit{bin\_tree} =
    1.60 -\{\!\begin{aligned}[t]
    1.61 -& \xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \\[-2pt]
    1.62 -& \textit{Branch}~\xi_1~\xi_2,\> \unr\}\end{aligned}$ \\
    1.63 -\hbox{}\qquad {\slshape Constants:} \nopagebreak \\
    1.64 -\hbox{}\qquad\qquad $\textit{labels} = \unkef
    1.65 -    (\!\begin{aligned}[t]%
    1.66 -    & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
    1.67 -    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
    1.68 -\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \unkef
    1.69 -    (\!\begin{aligned}[t]%
    1.70 -    & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
    1.71 -    & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
    1.72 -The existence of a nonstandard model suggests that the induction hypothesis is not general enough or may even
    1.73 -be wrong. See the Nitpick manual's ``Inductive Properties'' section for details (``\textit{isabelle doc nitpick}'').
    1.74 -\postw
    1.75 -
    1.76 -Reading the Nitpick manual is a most excellent idea.
    1.77 -But what's going on? The \textit{non\_std} option told the tool to look for
    1.78 -nonstandard models of binary trees, which means that new ``nonstandard'' trees
    1.79 -$\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
    1.80 -generated by the \textit{Leaf} and \textit{Branch} constructors.%
    1.81 -\footnote{Notice the similarity between allowing nonstandard trees here and
    1.82 -allowing unreachable states in the preceding example (by removing the ``$n \in
    1.83 -\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
    1.84 -set of objects over which the induction is performed while doing the step
    1.85 -in order to test the induction hypothesis's strength.}
    1.86 -Unlike standard trees, these new trees contain cycles. We will see later that
    1.87 -every property of acyclic trees that can be proved without using induction also
    1.88 -holds for cyclic trees. Hence,
    1.89 -%
    1.90 -\begin{quote}
    1.91 -\textsl{If the induction
    1.92 -hypothesis is strong enough, the induction step will hold even for nonstandard
    1.93 -objects, and Nitpick won't find any nonstandard counterexample.}
    1.94 -\end{quote}
    1.95 -%
    1.96 -But here the tool find some nonstandard trees $t = \xi_1$
    1.97 -and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
    1.98 -\textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
    1.99 -Because neither tree contains both $a$ and $b$, the induction hypothesis tells
   1.100 -us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
   1.101 -and as a result we know nothing about the labels of the tree
   1.102 -$\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
   1.103 -$\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
   1.104 -labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
   1.105 -\textit{labels}$ $(\textit{swap}~u~a~b)$.
   1.106 -
   1.107 -The solution is to ensure that we always know what the labels of the subtrees
   1.108 -are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
   1.109 -$t$ in the statement of the lemma:
   1.110 -
   1.111 -\prew
   1.112 -\textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~a~b) = {}$ \\
   1.113 -\phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \nopagebreak \\
   1.114 -\phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~\textit{labels}~t~\textrm{else}~(\textit{labels}~t - \{a\}) \mathrel{\cup} \{b\}$ \\
   1.115 -\phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
   1.116 -\phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~(\textit{labels}~t - \{b\}) \mathrel{\cup} \{a\}~\textrm{else}~\textit{labels}~t)$''
   1.117 -\postw
   1.118 -
   1.119 -This time, Nitpick won't find any nonstandard counterexample, and we can perform
   1.120 -the induction step using \textit{auto}.
   1.121 -
   1.122  \section{Case Studies}
   1.123  \label{case-studies}
   1.124  
   1.125 @@ -2172,15 +2057,6 @@
   1.126  theoretical chance of finding a counterexample.
   1.127  
   1.128  {\small See also \textit{mono} (\S\ref{scope-of-search}).}
   1.129 -
   1.130 -\opargbool{std}{type}{non\_std}
   1.131 -Specifies whether the given (recursive) datatype should be given standard
   1.132 -models. Nonstandard models are unsound but can help debug structural induction
   1.133 -proofs, as explained in \S\ref{inductive-properties}.
   1.134 -
   1.135 -\optrue{std}{non\_std}
   1.136 -Specifies the default standardness to use. This can be overridden on a per-type
   1.137 -basis using the \textit{std}~\qty{type} option described above.
   1.138  \end{enum}
   1.139  
   1.140  \subsection{Output Format}
     2.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 16:44:46 2014 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     2.5      Author:     Jasmin Blanchette, TU Muenchen
     2.6 -    Copyright   2009-2013
     2.7 +    Copyright   2009-2014
     2.8  
     2.9  Examples from the Nitpick manual.
    2.10  *)
    2.11 @@ -15,10 +15,12 @@
    2.12  imports Main Real "~~/src/HOL/Library/Quotient_Product"
    2.13  begin
    2.14  
    2.15 -chapter {* 2. First Steps *}
    2.16 +
    2.17 +section {* 2. First Steps *}
    2.18  
    2.19  nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    2.20  
    2.21 +
    2.22  subsection {* 2.1. Propositional Logic *}
    2.23  
    2.24  lemma "P \<longleftrightarrow> Q"
    2.25 @@ -28,12 +30,14 @@
    2.26  nitpick [expect = genuine] 2
    2.27  oops
    2.28  
    2.29 +
    2.30  subsection {* 2.2. Type Variables *}
    2.31  
    2.32  lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
    2.33  nitpick [verbose, expect = genuine]
    2.34  oops
    2.35  
    2.36 +
    2.37  subsection {* 2.3. Constants *}
    2.38  
    2.39  lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
    2.40 @@ -47,6 +51,7 @@
    2.41  (* sledgehammer *)
    2.42  by (metis the_equality)
    2.43  
    2.44 +
    2.45  subsection {* 2.4. Skolemization *}
    2.46  
    2.47  lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
    2.48 @@ -61,6 +66,7 @@
    2.49  nitpick [expect = genuine]
    2.50  oops
    2.51  
    2.52 +
    2.53  subsection {* 2.5. Natural Numbers and Integers *}
    2.54  
    2.55  lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    2.56 @@ -81,6 +87,7 @@
    2.57  nitpick [card nat = 2, expect = none]
    2.58  oops
    2.59  
    2.60 +
    2.61  subsection {* 2.6. Inductive Datatypes *}
    2.62  
    2.63  lemma "hd (xs @ [y, y]) = hd xs"
    2.64 @@ -92,6 +99,7 @@
    2.65  nitpick [show_datatypes, expect = genuine]
    2.66  oops
    2.67  
    2.68 +
    2.69  subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
    2.70  
    2.71  definition "three = {0\<Colon>nat, 1, 2}"
    2.72 @@ -149,6 +157,7 @@
    2.73  nitpick [show_datatypes, expect = genuine]
    2.74  oops
    2.75  
    2.76 +
    2.77  subsection {* 2.8. Inductive and Coinductive Predicates *}
    2.78  
    2.79  inductive even where
    2.80 @@ -191,6 +200,7 @@
    2.81  nitpick [card nat = 4, show_consts, expect = genuine]
    2.82  oops
    2.83  
    2.84 +
    2.85  subsection {* 2.9. Coinductive Datatypes *}
    2.86  
    2.87  codatatype 'a llist = LNil | LCons 'a "'a llist"
    2.88 @@ -211,6 +221,7 @@
    2.89  nitpick [card = 1\<emdash>5, expect = none]
    2.90  sorry
    2.91  
    2.92 +
    2.93  subsection {* 2.10. Boxing *}
    2.94  
    2.95  datatype tm = Var nat | Lam tm | App tm tm
    2.96 @@ -247,6 +258,7 @@
    2.97  nitpick [card = 1\<emdash>5, expect = none]
    2.98  sorry
    2.99  
   2.100 +
   2.101  subsection {* 2.11. Scope Monotonicity *}
   2.102  
   2.103  lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
   2.104 @@ -258,6 +270,7 @@
   2.105  nitpick [expect = genuine]
   2.106  oops
   2.107  
   2.108 +
   2.109  subsection {* 2.12. Inductive Properties *}
   2.110  
   2.111  inductive_set reach where
   2.112 @@ -286,45 +299,12 @@
   2.113  lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
   2.114  by (induct set: reach) arith+
   2.115  
   2.116 -datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
   2.117 -
   2.118 -primrec labels where
   2.119 -"labels (Leaf a) = {a}" |
   2.120 -"labels (Branch t u) = labels t \<union> labels u"
   2.121 -
   2.122 -primrec swap where
   2.123 -"swap (Leaf c) a b =
   2.124 - (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
   2.125 -"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
   2.126 -
   2.127 -lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
   2.128 -(* nitpick *)
   2.129 -proof (induct t)
   2.130 -  case Leaf thus ?case by simp
   2.131 -next
   2.132 -  case (Branch t u) thus ?case
   2.133 -  (* nitpick *)
   2.134 -  nitpick [non_std, show_all, expect = genuine]
   2.135 -oops
   2.136 -
   2.137 -lemma "labels (swap t a b) =
   2.138 -       (if a \<in> labels t then
   2.139 -          if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
   2.140 -        else
   2.141 -          if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
   2.142 -(* nitpick *)
   2.143 -proof (induct t)
   2.144 -  case Leaf thus ?case by simp
   2.145 -next
   2.146 -  case (Branch t u) thus ?case
   2.147 -  nitpick [non_std, card = 1\<emdash>4, expect = none]
   2.148 -  by auto
   2.149 -qed
   2.150  
   2.151  section {* 3. Case Studies *}
   2.152  
   2.153  nitpick_params [max_potential = 0]
   2.154  
   2.155 +
   2.156  subsection {* 3.1. A Context-Free Grammar *}
   2.157  
   2.158  datatype alphabet = a | b
   2.159 @@ -399,6 +379,7 @@
   2.160  nitpick [card = 1\<emdash>5, expect = none]
   2.161  sorry
   2.162  
   2.163 +
   2.164  subsection {* 3.2. AA Trees *}
   2.165  
   2.166  datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
     3.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Mar 03 16:44:46 2014 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
     3.3 @@ -22,10 +22,9 @@
     3.4  
     3.5  val thy = @{theory}
     3.6  val ctxt = @{context}
     3.7 -val stds = [(NONE, true)]
     3.8  val subst = []
     3.9  val tac_timeout = seconds 1.0
    3.10 -val case_names = case_const_names ctxt stds
    3.11 +val case_names = case_const_names ctxt
    3.12  val defs = all_defs_of thy subst
    3.13  val nondefs = all_nondefs_of ctxt subst
    3.14  val def_tables = const_def_tables ctxt subst defs
    3.15 @@ -37,18 +36,17 @@
    3.16  val ground_thm_table = ground_theorem_table thy
    3.17  val ersatz_table = ersatz_table ctxt
    3.18  val hol_ctxt as {thy, ...} : hol_context =
    3.19 -  {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
    3.20 -   stds = stds, wfs = [], user_axioms = NONE, debug = false,
    3.21 -   whacks = [], binary_ints = SOME false, destroy_constrs = true,
    3.22 -   specialize = false, star_linear_preds = false, total_consts = NONE,
    3.23 -   needs = NONE, tac_timeout = tac_timeout, evals = [], case_names = case_names,
    3.24 -   def_tables = def_tables, nondef_table = nondef_table, nondefs = nondefs,
    3.25 -   simp_table = simp_table, psimp_table = psimp_table,
    3.26 -   choice_spec_table = choice_spec_table, intro_table = intro_table,
    3.27 -   ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    3.28 -   skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    3.29 -   unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    3.30 -   constr_cache = Unsynchronized.ref []}
    3.31 +  {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [], wfs = [],
    3.32 +   user_axioms = NONE, debug = false, whacks = [], binary_ints = SOME false,
    3.33 +   destroy_constrs = true, specialize = false, star_linear_preds = false,
    3.34 +   total_consts = NONE, needs = NONE, tac_timeout = tac_timeout, evals = [],
    3.35 +   case_names = case_names, def_tables = def_tables,
    3.36 +   nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
    3.37 +   psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    3.38 +   intro_table = intro_table, ground_thm_table = ground_thm_table,
    3.39 +   ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
    3.40 +   special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    3.41 +   wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
    3.42  val binarize = false
    3.43  
    3.44  fun is_mono t =
     4.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Mon Mar 03 16:44:46 2014 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4  (*  Title:      HOL/Tools/Nitpick/kodkod.ML
     4.5      Author:     Jasmin Blanchette, TU Muenchen
     4.6 -    Copyright   2008, 2009, 2010
     4.7 +    Copyright   2008-2014
     4.8  
     4.9  ML interface for Kodkod.
    4.10  *)
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 16:44:46 2014 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 22:33:22 2014 +0100
     5.3 @@ -21,7 +21,6 @@
     5.4       boxes: (typ option * bool option) list,
     5.5       finitizes: (typ option * bool option) list,
     5.6       monos: (typ option * bool option) list,
     5.7 -     stds: (typ option * bool) list,
     5.8       wfs: (styp option * bool option) list,
     5.9       sat_solver: string,
    5.10       blocking: bool,
    5.11 @@ -107,7 +106,6 @@
    5.12     boxes: (typ option * bool option) list,
    5.13     finitizes: (typ option * bool option) list,
    5.14     monos: (typ option * bool option) list,
    5.15 -   stds: (typ option * bool) list,
    5.16     wfs: (styp option * bool option) list,
    5.17     sat_solver: string,
    5.18     blocking: bool,
    5.19 @@ -227,8 +225,8 @@
    5.20              error "You must import the theory \"Nitpick\" to use Nitpick"
    5.21  *)
    5.22      val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
    5.23 -         boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    5.24 -         verbose, overlord, spy, user_axioms, assms, whacks, merge_type_vars,
    5.25 +         boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose,
    5.26 +         overlord, spy, user_axioms, assms, whacks, merge_type_vars,
    5.27           binary_ints, destroy_constrs, specialize, star_linear_preds,
    5.28           total_consts, needs, peephole_optim, datatype_sym_break,
    5.29           kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
    5.30 @@ -291,7 +289,7 @@
    5.31      val original_max_potential = max_potential
    5.32      val original_max_genuine = max_genuine
    5.33      val max_bisim_depth = fold Integer.max bisim_depths ~1
    5.34 -    val case_names = case_const_names ctxt stds
    5.35 +    val case_names = case_const_names ctxt
    5.36      val defs = def_assm_ts @ all_defs_of thy subst
    5.37      val nondefs = all_nondefs_of ctxt subst
    5.38      val def_tables = const_def_tables ctxt subst defs
    5.39 @@ -306,12 +304,11 @@
    5.40      val ersatz_table = ersatz_table ctxt
    5.41      val hol_ctxt as {wf_cache, ...} =
    5.42        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
    5.43 -       stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    5.44 -       whacks = whacks, binary_ints = binary_ints,
    5.45 -       destroy_constrs = destroy_constrs, specialize = specialize,
    5.46 -       star_linear_preds = star_linear_preds, total_consts = total_consts,
    5.47 -       needs = needs, tac_timeout = tac_timeout, evals = evals,
    5.48 -       case_names = case_names, def_tables = def_tables,
    5.49 +       wfs = wfs, user_axioms = user_axioms, debug = debug, whacks = whacks,
    5.50 +       binary_ints = binary_ints, destroy_constrs = destroy_constrs,
    5.51 +       specialize = specialize, star_linear_preds = star_linear_preds,
    5.52 +       total_consts = total_consts, needs = needs, tac_timeout = tac_timeout,
    5.53 +       evals = evals, case_names = case_names, def_tables = def_tables,
    5.54         nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
    5.55         psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    5.56         intro_table = intro_table, ground_thm_table = ground_thm_table,
    5.57 @@ -359,7 +356,6 @@
    5.58      val (sel_names, nonsel_names) =
    5.59        List.partition (is_sel o nickname_of) const_names
    5.60      val sound_finitizes = none_true finitizes
    5.61 -    val standard = forall snd stds
    5.62  (*
    5.63      val _ =
    5.64        List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us @ need_us)
    5.65 @@ -380,7 +376,7 @@
    5.66                   ". " ^ extra))
    5.67        end
    5.68      fun is_type_fundamentally_monotonic T =
    5.69 -      (is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso
    5.70 +      (is_datatype ctxt T andalso not (is_quot_type ctxt T) andalso
    5.71         (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
    5.72        is_number_type ctxt T orelse is_bit_type T
    5.73      fun is_type_actually_monotonic T =
    5.74 @@ -406,8 +402,7 @@
    5.75            SOME (SOME b) => b
    5.76          | _ => is_type_kind_of_monotonic T
    5.77      fun is_datatype_deep T =
    5.78 -      not standard orelse T = @{typ unit} orelse T = nat_T orelse
    5.79 -      is_word_type T orelse
    5.80 +      T = @{typ unit} orelse T = nat_T orelse is_word_type T orelse
    5.81        exists (curry (op =) T o domain_type o type_of) sel_names
    5.82      val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
    5.83                   |> sort Term_Ord.typ_ord
    5.84 @@ -416,7 +411,7 @@
    5.85           exists (member (op =) [nat_T, int_T]) all_Ts then
    5.86          print_v (K "The option \"binary_ints\" will be ignored because of the \
    5.87                     \presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \
    5.88 -                   \in the problem or because of the \"non_std\" option.")
    5.89 +                   \in the problem.")
    5.90        else
    5.91          ()
    5.92      val _ =
    5.93 @@ -441,7 +436,7 @@
    5.94        else
    5.95          ()
    5.96      val (deep_dataTs, shallow_dataTs) =
    5.97 -      all_Ts |> filter (is_datatype ctxt stds)
    5.98 +      all_Ts |> filter (is_datatype ctxt)
    5.99               |> List.partition is_datatype_deep
   5.100      val finitizable_dataTs =
   5.101        (deep_dataTs |> filter_out (is_finite_type hol_ctxt)
   5.102 @@ -454,26 +449,6 @@
   5.103                           "Nitpick can use a more precise finite encoding."))
   5.104        else
   5.105          ()
   5.106 -    (* This detection code is an ugly hack. Fortunately, it is used only to
   5.107 -       provide a hint to the user. *)
   5.108 -    fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
   5.109 -      not (null fixes) andalso
   5.110 -      exists (String.isSuffix ".hyps" o Name_Space.full_name Name_Space.default_naming o fst) assumes andalso
   5.111 -      exists (exists (curry (op =) name o shortest_name o fst)
   5.112 -              o datatype_constrs hol_ctxt) deep_dataTs
   5.113 -    val likely_in_struct_induct_step =
   5.114 -      exists is_struct_induct_step (Proof_Context.dest_cases ctxt)
   5.115 -    val _ = if standard andalso likely_in_struct_induct_step then
   5.116 -              pprint_nt (fn () => Pretty.blk (0,
   5.117 -                  pstrs "Hint: To check that the induction hypothesis is \
   5.118 -                        \general enough, try this command: " @
   5.119 -                  [Pretty.mark
   5.120 -                    (Active.make_markup Markup.sendbackN
   5.121 -                      {implicit = false, properties = [Markup.padding_command]})
   5.122 -                    (Pretty.blk (0,
   5.123 -                       pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
   5.124 -            else
   5.125 -              ()
   5.126  (*
   5.127      val _ = print_g "Monotonic types:"
   5.128      val _ = List.app (print_g o string_for_type ctxt) mono_Ts
   5.129 @@ -649,9 +624,7 @@
   5.130                    "scope.");
   5.131                NONE)
   5.132  
   5.133 -    val das_wort_model =
   5.134 -      (if falsify then "counterexample" else "model")
   5.135 -      |> not standard ? prefix "nonstandard "
   5.136 +    val das_wort_model = if falsify then "counterexample" else "model"
   5.137  
   5.138      val scopes = Unsynchronized.ref []
   5.139      val generated_scopes = Unsynchronized.ref []
   5.140 @@ -704,7 +677,7 @@
   5.141                Pretty.indent indent_size reconstructed_model]);
   5.142           print_t (K "% SZS output end FiniteModel");
   5.143           if genuine then
   5.144 -           (if check_genuine andalso standard then
   5.145 +           (if check_genuine then
   5.146                case prove_hol_model scope tac_timeout free_names sel_names
   5.147                                     rel_table bounds (assms_prop ()) of
   5.148                  SOME true =>
   5.149 @@ -722,13 +695,6 @@
   5.150                 | NONE => print "No confirmation by \"auto\"."
   5.151              else
   5.152                ();
   5.153 -            if not standard andalso likely_in_struct_induct_step then
   5.154 -              print "The existence of a nonstandard model suggests that the \
   5.155 -                    \induction hypothesis is not general enough or may even be \
   5.156 -                    \wrong. See the Nitpick manual's \"Inductive Properties\" \
   5.157 -                    \section for details (\"isabelle doc nitpick\")."
   5.158 -            else
   5.159 -              ();
   5.160              if has_lonely_bool_var orig_t then
   5.161                print "Hint: Maybe you forgot a colon after the lemma's name?"
   5.162              else if has_syntactic_sorts orig_t then
   5.163 @@ -1018,13 +984,8 @@
   5.164          else if max_genuine = original_max_genuine then
   5.165            if max_potential = original_max_potential then
   5.166              (print_t (K "% SZS status Unknown");
   5.167 -             print_nt (fn () =>
   5.168 -                 "Nitpick found no " ^ das_wort_model ^ "." ^
   5.169 -                 (if not standard andalso likely_in_struct_induct_step then
   5.170 -                    " This suggests that the induction hypothesis might be \
   5.171 -                    \general enough to prove this subgoal."
   5.172 -                  else
   5.173 -                    "")); if skipped > 0 then unknownN else noneN)
   5.174 +             print_nt (fn () => "Nitpick found no " ^ das_wort_model ^ ".");
   5.175 +             if skipped > 0 then unknownN else noneN)
   5.176            else
   5.177              (print_nt (fn () =>
   5.178                   excipit ("could not find a" ^
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Mar 03 16:44:46 2014 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Mar 03 22:33:22 2014 +0100
     6.3 @@ -48,7 +48,6 @@
     6.4     ("box", "smart"),
     6.5     ("finitize", "smart"),
     6.6     ("mono", "smart"),
     6.7 -   ("std", "true"),
     6.8     ("wf", "smart"),
     6.9     ("sat_solver", "smart"),
    6.10     ("batch_size", "smart"),
    6.11 @@ -85,7 +84,6 @@
    6.12    [("dont_box", "box"),
    6.13     ("dont_finitize", "finitize"),
    6.14     ("non_mono", "mono"),
    6.15 -   ("non_std", "std"),
    6.16     ("non_wf", "wf"),
    6.17     ("non_blocking", "blocking"),
    6.18     ("satisfy", "falsify"),
    6.19 @@ -115,8 +113,7 @@
    6.20                   "expect"] s orelse
    6.21    exists (fn p => String.isPrefix (p ^ " ") s)
    6.22           ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
    6.23 -          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
    6.24 -          "atoms"]
    6.25 +          "mono", "non_mono", "wf", "non_wf", "format", "atoms"]
    6.26  
    6.27  fun check_raw_param (s, _) =
    6.28    if is_known_raw_param s then ()
    6.29 @@ -218,8 +215,6 @@
    6.30      fun lookup_ints_assigns read prefix min_int =
    6.31        lookup_assigns read prefix (signed_string_of_int min_int)
    6.32                       (int_seq_from_string prefix min_int)
    6.33 -    fun lookup_bool_assigns read prefix =
    6.34 -      lookup_assigns read prefix "" (the o parse_bool_option false prefix)
    6.35      fun lookup_bool_option_assigns read prefix =
    6.36        lookup_assigns read prefix "" (parse_bool_option true prefix)
    6.37      fun lookup_strings_assigns read prefix =
    6.38 @@ -247,7 +242,6 @@
    6.39      val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
    6.40      val monos = if mode = Auto_Try then [(NONE, SOME true)]
    6.41                  else lookup_bool_option_assigns read_type_polymorphic "mono"
    6.42 -    val stds = lookup_bool_assigns read_type_polymorphic "std"
    6.43      val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
    6.44      val sat_solver = lookup_string "sat_solver"
    6.45      val blocking = mode <> Normal orelse lookup_bool "blocking"
    6.46 @@ -290,19 +284,24 @@
    6.47        | NONE => if debug then 1 else 50
    6.48      val expect = lookup_string "expect"
    6.49    in
    6.50 -    {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, iters_assigns = iters_assigns,
    6.51 -     bitss = bitss, bisim_depths = bisim_depths, boxes = boxes, finitizes = finitizes,
    6.52 -     monos = monos, stds = stds, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
    6.53 -     falsify = falsify, debug = debug, verbose = verbose, overlord = overlord, spy = spy,
    6.54 -     user_axioms = user_axioms, assms = assms, whacks = whacks, merge_type_vars = merge_type_vars,
    6.55 -     binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize,
    6.56 -     star_linear_preds = star_linear_preds, total_consts = total_consts, needs = needs,
    6.57 -     peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
    6.58 -     kodkod_sym_break = kodkod_sym_break, timeout = timeout, tac_timeout = tac_timeout,
    6.59 -     max_threads = max_threads, show_datatypes = show_datatypes, show_skolems = show_skolems,
    6.60 -     show_consts = show_consts, evals = evals, formats = formats, atomss = atomss,
    6.61 -     max_potential = max_potential, max_genuine = max_genuine, check_potential = check_potential,
    6.62 -     check_genuine = check_genuine, batch_size = batch_size, expect = expect}
    6.63 +    {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
    6.64 +     iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
    6.65 +     boxes = boxes, finitizes = finitizes, monos = monos, wfs = wfs,
    6.66 +     sat_solver = sat_solver, blocking = blocking, falsify = falsify,
    6.67 +     debug = debug, verbose = verbose, overlord = overlord, spy = spy,
    6.68 +     user_axioms = user_axioms, assms = assms, whacks = whacks,
    6.69 +     merge_type_vars = merge_type_vars, binary_ints = binary_ints,
    6.70 +     destroy_constrs = destroy_constrs, specialize = specialize,
    6.71 +     star_linear_preds = star_linear_preds, total_consts = total_consts,
    6.72 +     needs = needs, peephole_optim = peephole_optim,
    6.73 +     datatype_sym_break = datatype_sym_break,
    6.74 +     kodkod_sym_break = kodkod_sym_break, timeout = timeout,
    6.75 +     tac_timeout = tac_timeout, max_threads = max_threads,
    6.76 +     show_datatypes = show_datatypes, show_skolems = show_skolems,
    6.77 +     show_consts = show_consts, evals = evals, formats = formats,
    6.78 +     atomss = atomss, max_potential = max_potential, max_genuine = max_genuine,
    6.79 +     check_potential = check_potential, check_genuine = check_genuine,
    6.80 +     batch_size = batch_size, expect = expect}
    6.81    end
    6.82  
    6.83  fun default_params thy =
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 16:44:46 2014 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 22:33:22 2014 +0100
     7.3 @@ -18,7 +18,6 @@
     7.4       ctxt: Proof.context,
     7.5       max_bisim_depth: int,
     7.6       boxes: (typ option * bool option) list,
     7.7 -     stds: (typ option * bool) list,
     7.8       wfs: (styp option * bool option) list,
     7.9       user_axioms: bool option,
    7.10       debug: bool,
    7.11 @@ -114,12 +113,11 @@
    7.12    val mk_flat_tuple : typ -> term list -> term
    7.13    val dest_n_tuple : int -> term -> term list
    7.14    val is_real_datatype : theory -> string -> bool
    7.15 -  val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
    7.16    val is_codatatype : Proof.context -> typ -> bool
    7.17    val is_quot_type : Proof.context -> typ -> bool
    7.18    val is_pure_typedef : Proof.context -> typ -> bool
    7.19    val is_univ_typedef : Proof.context -> typ -> bool
    7.20 -  val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
    7.21 +  val is_datatype : Proof.context -> typ -> bool
    7.22    val is_record_constr : styp -> bool
    7.23    val is_record_get : theory -> styp -> bool
    7.24    val is_record_update : theory -> styp -> bool
    7.25 @@ -130,7 +128,7 @@
    7.26    val mate_of_rep_fun : Proof.context -> styp -> styp
    7.27    val is_constr_like : Proof.context -> styp -> bool
    7.28    val is_constr_like_injective : Proof.context -> styp -> bool
    7.29 -  val is_constr : Proof.context -> (typ option * bool) list -> styp -> bool
    7.30 +  val is_constr : Proof.context -> styp -> bool
    7.31    val is_sel : string -> bool
    7.32    val is_sel_like_and_no_discr : string -> bool
    7.33    val box_type : hol_context -> boxability -> typ -> typ
    7.34 @@ -182,22 +180,17 @@
    7.35    val s_betapplys : typ list -> term * term list -> term
    7.36    val discriminate_value : hol_context -> styp -> term -> term
    7.37    val select_nth_constr_arg :
    7.38 -    Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
    7.39 -    -> term
    7.40 -  val construct_value :
    7.41 -    Proof.context -> (typ option * bool) list -> styp -> term list -> term
    7.42 +    Proof.context -> styp -> term -> int -> typ -> term
    7.43 +  val construct_value : Proof.context -> styp -> term list -> term
    7.44    val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
    7.45    val special_bounds : term list -> (indexname * typ) list
    7.46    val is_funky_typedef : Proof.context -> typ -> bool
    7.47    val all_defs_of : theory -> (term * term) list -> term list
    7.48    val all_nondefs_of : Proof.context -> (term * term) list -> term list
    7.49 -  val arity_of_built_in_const :
    7.50 -    theory -> (typ option * bool) list -> styp -> int option
    7.51 -  val is_built_in_const :
    7.52 -    theory -> (typ option * bool) list -> styp -> bool
    7.53 +  val arity_of_built_in_const : styp -> int option
    7.54 +  val is_built_in_const : styp -> bool
    7.55    val term_under_def : term -> term
    7.56 -  val case_const_names :
    7.57 -    Proof.context -> (typ option * bool) list -> (string * int) list
    7.58 +  val case_const_names : Proof.context -> (string * int) list
    7.59    val unfold_defs_in_term : hol_context -> term -> term
    7.60    val const_def_tables :
    7.61      Proof.context -> (term * term) list -> term list
    7.62 @@ -216,7 +209,7 @@
    7.63    val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list
    7.64    val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
    7.65    val optimized_quot_type_axioms :
    7.66 -    Proof.context -> (typ option * bool) list -> string * typ list -> term list
    7.67 +    Proof.context -> string * typ list -> term list
    7.68    val def_of_const : theory -> const_table * const_table -> styp -> term option
    7.69    val fixpoint_kind_of_rhs : term -> fixpoint_kind
    7.70    val fixpoint_kind_of_const :
    7.71 @@ -259,7 +252,6 @@
    7.72     ctxt: Proof.context,
    7.73     max_bisim_depth: int,
    7.74     boxes: (typ option * bool option) list,
    7.75 -   stds: (typ option * bool) list,
    7.76     wfs: (styp option * bool option) list,
    7.77     user_axioms: bool option,
    7.78     debug: bool,
    7.79 @@ -397,14 +389,22 @@
    7.80     (@{const_name is_unknown}, 1),
    7.81     (@{const_name safe_The}, 1),
    7.82     (@{const_name Nitpick.Frac}, 0),
    7.83 -   (@{const_name Nitpick.norm_frac}, 0)]
    7.84 -val built_in_nat_consts =
    7.85 -  [(@{const_name Suc}, 0),
    7.86 +   (@{const_name Nitpick.norm_frac}, 0),
    7.87 +   (@{const_name Suc}, 0),
    7.88     (@{const_name nat}, 0),
    7.89     (@{const_name Nitpick.nat_gcd}, 0),
    7.90     (@{const_name Nitpick.nat_lcm}, 0)]
    7.91  val built_in_typed_consts =
    7.92 -  [((@{const_name zero_class.zero}, int_T), 0),
    7.93 +  [((@{const_name zero_class.zero}, nat_T), 0),
    7.94 +   ((@{const_name one_class.one}, nat_T), 0),
    7.95 +   ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
    7.96 +   ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
    7.97 +   ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
    7.98 +   ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
    7.99 +   ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
   7.100 +   ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
   7.101 +   ((@{const_name of_nat}, nat_T --> int_T), 0),
   7.102 +   ((@{const_name zero_class.zero}, int_T), 0),
   7.103     ((@{const_name one_class.one}, int_T), 0),
   7.104     ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
   7.105     ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
   7.106 @@ -413,16 +413,6 @@
   7.107     ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
   7.108     ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
   7.109     ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
   7.110 -val built_in_typed_nat_consts =
   7.111 -  [((@{const_name zero_class.zero}, nat_T), 0),
   7.112 -   ((@{const_name one_class.one}, nat_T), 0),
   7.113 -   ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
   7.114 -   ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
   7.115 -   ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
   7.116 -   ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
   7.117 -   ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
   7.118 -   ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
   7.119 -   ((@{const_name of_nat}, nat_T --> int_T), 0)]
   7.120  val built_in_set_like_consts =
   7.121    [(@{const_name ord_class.less_eq}, 2)]
   7.122  
   7.123 @@ -583,14 +573,13 @@
   7.124  
   7.125  val is_typedef = is_some oo typedef_info
   7.126  val is_real_datatype = is_some oo Datatype.get_info
   7.127 -fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
   7.128  
   7.129  (* FIXME: Use antiquotation for "natural" below or detect "rep_datatype",
   7.130     e.g., by adding a field to "Datatype_Aux.info". *)
   7.131 -fun is_basic_datatype thy stds s =
   7.132 +val is_basic_datatype =
   7.133    member (op =) [@{type_name prod}, @{type_name set}, @{type_name bool},
   7.134 -                 @{type_name int}, @{type_name natural}, @{type_name integer}] s orelse
   7.135 -  (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
   7.136 +                 @{type_name nat}, @{type_name int}, @{type_name natural},
   7.137 +                 @{type_name integer}]
   7.138  
   7.139  fun repair_constr_type (Type (_, Ts)) T =
   7.140    snd (dest_Const (Ctr_Sugar.mk_ctr Ts (Const (Name.uu, T))))
   7.141 @@ -626,14 +615,12 @@
   7.142  
   7.143  fun register_codatatype_generic coT case_name constr_xs generic =
   7.144    let
   7.145 -    val thy = Context.theory_of generic
   7.146      val {frac_types, ersatz_table, codatatypes} = Data.get generic
   7.147      val constr_xs = map (apsnd (repair_constr_type coT)) constr_xs
   7.148      val (co_s, coTs) = dest_Type coT
   7.149      val _ =
   7.150        if forall is_TFree coTs andalso not (has_duplicates (op =) coTs) andalso
   7.151 -         co_s <> @{type_name fun} andalso
   7.152 -         not (is_basic_datatype thy [(NONE, true)] co_s) then
   7.153 +         co_s <> @{type_name fun} andalso not (is_basic_datatype co_s) then
   7.154          ()
   7.155        else
   7.156          raise TYPE ("Nitpick_HOL.register_codatatype_generic", [coT], [])
   7.157 @@ -696,13 +683,11 @@
   7.158         end
   7.159       | NONE => false)
   7.160    | is_univ_typedef _ _ = false
   7.161 -fun is_datatype ctxt stds (T as Type (s, _)) =
   7.162 -    let val thy = Proof_Context.theory_of ctxt in
   7.163 -      (is_typedef ctxt s orelse is_registered_type ctxt T orelse
   7.164 -       T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
   7.165 -      not (is_basic_datatype thy stds s)
   7.166 -    end
   7.167 -  | is_datatype _ _ _ = false
   7.168 +fun is_datatype ctxt (T as Type (s, _)) =
   7.169 +    (is_typedef ctxt s orelse is_registered_type ctxt T orelse
   7.170 +     T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
   7.171 +    not (is_basic_datatype s)
   7.172 +  | is_datatype _ _ = false
   7.173  
   7.174  fun all_record_fields thy T =
   7.175    let val (recs, more) = Record.get_extT_fields thy T in
   7.176 @@ -818,13 +803,10 @@
   7.177  fun is_stale_constr ctxt (x as (s, T)) =
   7.178    is_registered_type ctxt (body_type T) andalso is_constr_like ctxt x andalso
   7.179    not (s = @{const_name Nitpick.Abs_Frac} orelse is_coconstr ctxt x)
   7.180 -fun is_constr ctxt stds (x as (_, T)) =
   7.181 -  let val thy = Proof_Context.theory_of ctxt in
   7.182 -    is_constr_like ctxt x andalso
   7.183 -    not (is_basic_datatype thy stds
   7.184 -                         (fst (dest_Type (unarize_type (body_type T))))) andalso
   7.185 -    not (is_stale_constr ctxt x)
   7.186 -  end
   7.187 +fun is_constr ctxt (x as (_, T)) =
   7.188 +  is_constr_like ctxt x andalso
   7.189 +  not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
   7.190 +  not (is_stale_constr ctxt x)
   7.191  val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   7.192  val is_sel_like_and_no_discr =
   7.193    String.isPrefix sel_prefix orf
   7.194 @@ -927,7 +909,7 @@
   7.195  fun zero_const T = Const (@{const_name zero_class.zero}, T)
   7.196  fun suc_const T = Const (@{const_name Suc}, T --> T)
   7.197  
   7.198 -fun uncached_datatype_constrs ({thy, ctxt, stds, ...} : hol_context)
   7.199 +fun uncached_datatype_constrs ({thy, ctxt, ...} : hol_context)
   7.200                                (T as Type (s, Ts)) =
   7.201      (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
   7.202                         s of
   7.203 @@ -944,7 +926,7 @@
   7.204                [(Abs_name,
   7.205                  varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   7.206              | NONE => [] (* impossible *)
   7.207 -          else if is_datatype ctxt stds T then
   7.208 +          else if is_datatype ctxt T then
   7.209              case Datatype.get_info thy s of
   7.210                SOME {index, descr, ...} =>
   7.211                let
   7.212 @@ -1179,9 +1161,9 @@
   7.213      else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
   7.214    | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
   7.215  
   7.216 -fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
   7.217 +fun nth_arg_sel_term_for_constr (x as (s, T)) n =
   7.218    let val (arg_Ts, dataT) = strip_type T in
   7.219 -    if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
   7.220 +    if dataT = nat_T then
   7.221        @{term "%n::nat. n - 1"}
   7.222      else if is_pair_type dataT then
   7.223        Const (nth_sel_for_constr x n)
   7.224 @@ -1199,30 +1181,26 @@
   7.225                       (List.take (arg_Ts, n)) 0
   7.226        in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
   7.227    end
   7.228 -fun select_nth_constr_arg ctxt stds x t n res_T =
   7.229 -  let val thy = Proof_Context.theory_of ctxt in
   7.230 -    (case strip_comb t of
   7.231 -       (Const x', args) =>
   7.232 -       if x = x' then
   7.233 -          if is_constr_like_injective ctxt x then nth args n else raise SAME ()
   7.234 -       else if is_constr_like ctxt x' then
   7.235 -         Const (@{const_name unknown}, res_T)
   7.236 -       else
   7.237 -         raise SAME ()
   7.238 -     | _ => raise SAME())
   7.239 -    handle SAME () =>
   7.240 -           s_betapply [] (nth_arg_sel_term_for_constr thy stds x n, t)
   7.241 -  end
   7.242 +fun select_nth_constr_arg ctxt x t n res_T =
   7.243 +  (case strip_comb t of
   7.244 +     (Const x', args) =>
   7.245 +     if x = x' then
   7.246 +        if is_constr_like_injective ctxt x then nth args n else raise SAME ()
   7.247 +     else if is_constr_like ctxt x' then
   7.248 +       Const (@{const_name unknown}, res_T)
   7.249 +     else
   7.250 +       raise SAME ()
   7.251 +   | _ => raise SAME())
   7.252 +  handle SAME () => s_betapply [] (nth_arg_sel_term_for_constr x n, t)
   7.253  
   7.254 -fun construct_value _ _ x [] = Const x
   7.255 -  | construct_value ctxt stds (x as (s, _)) args =
   7.256 +fun construct_value _ x [] = Const x
   7.257 +  | construct_value ctxt (x as (s, _)) args =
   7.258      let val args = map Envir.eta_contract args in
   7.259        case hd args of
   7.260          Const (s', _) $ t =>
   7.261          if is_sel_like_and_no_discr s' andalso
   7.262             constr_name_for_sel_like s' = s andalso
   7.263 -           forall (fn (n, t') =>
   7.264 -                      select_nth_constr_arg ctxt stds x t n dummyT = t')
   7.265 +           forall (fn (n, t') => select_nth_constr_arg ctxt x t n dummyT = t')
   7.266                    (index_seq 0 (length args) ~~ args) then
   7.267            t
   7.268          else
   7.269 @@ -1230,7 +1208,7 @@
   7.270        | _ => list_comb (Const x, args)
   7.271      end
   7.272  
   7.273 -fun constr_expand (hol_ctxt as {ctxt, stds, ...}) T t =
   7.274 +fun constr_expand (hol_ctxt as {ctxt, ...}) T t =
   7.275    (case head_of t of
   7.276       Const x => if is_constr_like ctxt x then t else raise SAME ()
   7.277     | _ => raise SAME ())
   7.278 @@ -1245,7 +1223,7 @@
   7.279                 datatype_constrs hol_ctxt T |> hd
   7.280             val arg_Ts = binder_types T'
   7.281           in
   7.282 -           list_comb (Const x', map2 (select_nth_constr_arg ctxt stds x' t)
   7.283 +           list_comb (Const x', map2 (select_nth_constr_arg ctxt x' t)
   7.284                                       (index_seq 0 (length arg_Ts)) arg_Ts)
   7.285           end
   7.286  
   7.287 @@ -1257,7 +1235,7 @@
   7.288    | _ => t
   7.289  fun coerce_bound_0_in_term hol_ctxt new_T old_T =
   7.290    old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
   7.291 -and coerce_term (hol_ctxt as {ctxt, stds, ...}) Ts new_T old_T t =
   7.292 +and coerce_term (hol_ctxt as {ctxt, ...}) Ts new_T old_T t =
   7.293    if old_T = new_T then
   7.294      t
   7.295    else
   7.296 @@ -1271,7 +1249,7 @@
   7.297                   |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
   7.298           |> Envir.eta_contract
   7.299           |> new_s <> @{type_name fun}
   7.300 -            ? construct_value ctxt stds
   7.301 +            ? construct_value ctxt
   7.302                    (@{const_name FunBox},
   7.303                     Type (@{type_name fun}, new_Ts) --> new_T)
   7.304                o single
   7.305 @@ -1285,12 +1263,12 @@
   7.306            if new_s = @{type_name fun} then
   7.307              coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
   7.308            else
   7.309 -            construct_value ctxt stds
   7.310 +            construct_value ctxt
   7.311                  (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
   7.312                  [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
   7.313                               (Type (@{type_name fun}, old_Ts)) t1]
   7.314          | Const _ $ t1 $ t2 =>
   7.315 -          construct_value ctxt stds
   7.316 +          construct_value ctxt
   7.317                (if new_s = @{type_name prod} then @{const_name Pair}
   7.318                 else @{const_name PairBox}, new_Ts ---> new_T)
   7.319                (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
   7.320 @@ -1343,33 +1321,27 @@
   7.321         |> filter_out (is_built_in_theory o theory_of_thm)
   7.322         |> map (subst_atomic subst o prop_of)
   7.323  
   7.324 -fun arity_of_built_in_const thy stds (s, T) =
   7.325 +fun arity_of_built_in_const (s, T) =
   7.326    if s = @{const_name If} then
   7.327      if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
   7.328    else
   7.329 -    let val std_nats = is_standard_datatype thy stds nat_T in
   7.330 -      case AList.lookup (op =)
   7.331 -                    (built_in_consts
   7.332 -                     |> std_nats ? append built_in_nat_consts) s of
   7.333 +    case AList.lookup (op =) built_in_consts s of
   7.334 +      SOME n => SOME n
   7.335 +    | NONE =>
   7.336 +      case AList.lookup (op =) built_in_typed_consts (s, unarize_type T) of
   7.337          SOME n => SOME n
   7.338        | NONE =>
   7.339 -        case AList.lookup (op =)
   7.340 -                 (built_in_typed_consts
   7.341 -                  |> std_nats ? append built_in_typed_nat_consts)
   7.342 -                 (s, unarize_type T) of
   7.343 -          SOME n => SOME n
   7.344 -        | NONE =>
   7.345 -          case s of
   7.346 -            @{const_name zero_class.zero} =>
   7.347 -            if is_iterator_type T then SOME 0 else NONE
   7.348 -          | @{const_name Suc} =>
   7.349 -            if is_iterator_type (domain_type T) then SOME 0 else NONE
   7.350 -          | _ => if is_fun_type T andalso is_set_like_type (domain_type T) then
   7.351 -                   AList.lookup (op =) built_in_set_like_consts s
   7.352 -                 else
   7.353 -                   NONE
   7.354 -    end
   7.355 -val is_built_in_const = is_some ooo arity_of_built_in_const
   7.356 +        case s of
   7.357 +          @{const_name zero_class.zero} =>
   7.358 +          if is_iterator_type T then SOME 0 else NONE
   7.359 +        | @{const_name Suc} =>
   7.360 +          if is_iterator_type (domain_type T) then SOME 0 else NONE
   7.361 +        | _ => if is_fun_type T andalso is_set_like_type (domain_type T) then
   7.362 +                 AList.lookup (op =) built_in_set_like_consts s
   7.363 +               else
   7.364 +                 NONE
   7.365 +
   7.366 +val is_built_in_const = is_some o arity_of_built_in_const
   7.367  
   7.368  (* This function is designed to work for both real definition axioms and
   7.369     simplification rules (equational specifications). *)
   7.370 @@ -1386,8 +1358,8 @@
   7.371  (* Here we crucially rely on "specialize_type" performing a preorder traversal
   7.372     of the term, without which the wrong occurrence of a constant could be
   7.373     matched in the face of overloading. *)
   7.374 -fun def_props_for_const thy stds table (x as (s, _)) =
   7.375 -  if is_built_in_const thy stds x then
   7.376 +fun def_props_for_const thy table (x as (s, _)) =
   7.377 +  if is_built_in_const x then
   7.378      []
   7.379    else
   7.380      these (Symtab.lookup table s)
   7.381 @@ -1409,12 +1381,12 @@
   7.382    in fold_rev aux args (SOME rhs) end
   7.383  
   7.384  fun get_def_of_const thy table (x as (s, _)) =
   7.385 -  x |> def_props_for_const thy [(NONE, false)] table |> List.last
   7.386 +  x |> def_props_for_const thy table |> List.last
   7.387      |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
   7.388    handle List.Empty => NONE
   7.389  
   7.390  fun def_of_const_ext thy (unfold_table, fallback_table) (x as (s, _)) =
   7.391 -  if is_built_in_const thy [(NONE, false)] x orelse original_name s <> s then
   7.392 +  if is_built_in_const x orelse original_name s <> s then
   7.393      NONE
   7.394    else case get_def_of_const thy unfold_table x of
   7.395      SOME def => SOME (true, def)
   7.396 @@ -1454,10 +1426,10 @@
   7.397                   | NONE => t)
   7.398                 | t => t)
   7.399  
   7.400 -fun case_const_names ctxt stds =
   7.401 +fun case_const_names ctxt =
   7.402    let val thy = Proof_Context.theory_of ctxt in
   7.403      Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
   7.404 -                    if is_basic_datatype thy stds dtype_s then
   7.405 +                    if is_basic_datatype dtype_s then
   7.406                        I
   7.407                      else
   7.408                        cons (case_name, AList.lookup (op =) descr index
   7.409 @@ -1473,14 +1445,14 @@
   7.410    end
   7.411  
   7.412  fun fixpoint_kind_of_const thy table x =
   7.413 -  if is_built_in_const thy [(NONE, false)] x then NoFp
   7.414 +  if is_built_in_const x then NoFp
   7.415    else fixpoint_kind_of_rhs (the (def_of_const thy table x))
   7.416    handle Option.Option => NoFp
   7.417  
   7.418 -fun is_real_inductive_pred ({thy, stds, def_tables, intro_table, ...}
   7.419 -                            : hol_context) x =
   7.420 +fun is_real_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context)
   7.421 +                           x =
   7.422    fixpoint_kind_of_const thy def_tables x <> NoFp andalso
   7.423 -  not (null (def_props_for_const thy stds intro_table x))
   7.424 +  not (null (def_props_for_const thy intro_table x))
   7.425  fun is_inductive_pred hol_ctxt (x as (s, _)) =
   7.426    is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
   7.427    String.isPrefix lbfp_prefix s
   7.428 @@ -1565,18 +1537,18 @@
   7.429                      exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
   7.430                  choice_spec_table
   7.431  
   7.432 -fun is_real_equational_fun ({thy, stds, simp_table, psimp_table, ...}
   7.433 +fun is_real_equational_fun ({thy, simp_table, psimp_table, ...}
   7.434                              : hol_context) x =
   7.435 -  exists (fn table => not (null (def_props_for_const thy stds table x)))
   7.436 +  exists (fn table => not (null (def_props_for_const thy table x)))
   7.437           [!simp_table, psimp_table]
   7.438  fun is_equational_fun_but_no_plain_def hol_ctxt =
   7.439    is_real_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt
   7.440  
   7.441  (** Constant unfolding **)
   7.442  
   7.443 -fun constr_case_body ctxt stds Ts (func_t, (x as (_, T))) =
   7.444 +fun constr_case_body ctxt Ts (func_t, (x as (_, T))) =
   7.445    let val arg_Ts = binder_types T in
   7.446 -    s_betapplys Ts (func_t, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
   7.447 +    s_betapplys Ts (func_t, map2 (select_nth_constr_arg ctxt x (Bound 0))
   7.448                                   (index_seq 0 (length arg_Ts)) arg_Ts)
   7.449    end
   7.450  fun add_constr_case res_T (body_t, guard_t) res_t =
   7.451 @@ -1585,13 +1557,13 @@
   7.452    else
   7.453      Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
   7.454      $ guard_t $ body_t $ res_t
   7.455 -fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) Ts dataT res_T func_ts =
   7.456 +fun optimized_case_def (hol_ctxt as {ctxt, ...}) Ts dataT res_T func_ts =
   7.457    let
   7.458      val xs = datatype_constrs hol_ctxt dataT
   7.459      val cases =
   7.460        func_ts ~~ xs
   7.461        |> map (fn (func_t, x) =>
   7.462 -                 (constr_case_body ctxt stds (dataT :: Ts)
   7.463 +                 (constr_case_body ctxt (dataT :: Ts)
   7.464                                     (incr_boundvars 1 func_t, x),
   7.465                    discriminate_value hol_ctxt x (Bound 0)))
   7.466        |> AList.group (op aconv)
   7.467 @@ -1613,7 +1585,7 @@
   7.468    end
   7.469    |> absdummy dataT
   7.470  
   7.471 -fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
   7.472 +fun optimized_record_get (hol_ctxt as {thy, ctxt, ...}) s rec_T res_T t =
   7.473    let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
   7.474      case no_of_record_field thy s rec_T of
   7.475        ~1 => (case rec_T of
   7.476 @@ -1622,14 +1594,14 @@
   7.477                   val rec_T' = List.last Ts
   7.478                   val j = num_record_fields thy rec_T - 1
   7.479                 in
   7.480 -                 select_nth_constr_arg ctxt stds constr_x t j res_T
   7.481 +                 select_nth_constr_arg ctxt constr_x t j res_T
   7.482                   |> optimized_record_get hol_ctxt s rec_T' res_T
   7.483                 end
   7.484               | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
   7.485                                  []))
   7.486 -    | j => select_nth_constr_arg ctxt stds constr_x t j res_T
   7.487 +    | j => select_nth_constr_arg ctxt constr_x t j res_T
   7.488    end
   7.489 -fun optimized_record_update (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T fun_t
   7.490 +fun optimized_record_update (hol_ctxt as {thy, ctxt, ...}) s rec_T fun_t
   7.491                              rec_t =
   7.492    let
   7.493      val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
   7.494 @@ -1638,7 +1610,7 @@
   7.495      val special_j = no_of_record_field thy s rec_T
   7.496      val ts =
   7.497        map2 (fn j => fn T =>
   7.498 -               let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in
   7.499 +               let val t = select_nth_constr_arg ctxt constr_x rec_t j T in
   7.500                   if j = special_j then
   7.501                     s_betapply [] (fun_t, t)
   7.502                   else if j = n - 1 andalso special_j = ~1 then
   7.503 @@ -1660,7 +1632,7 @@
   7.504  val def_inline_threshold_for_non_booleans = 20
   7.505  
   7.506  fun unfold_defs_in_term
   7.507 -        (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
   7.508 +        (hol_ctxt as {thy, ctxt, whacks, total_consts, case_names,
   7.509                        def_tables, ground_thm_table, ersatz_table, ...}) =
   7.510    let
   7.511      fun do_numeral depth Ts mult T some_t0 t1 t2 =
   7.512 @@ -1675,8 +1647,7 @@
   7.513                 val s = numeral_prefix ^ signed_string_of_int j
   7.514               in
   7.515                 if is_integer_like_type T then
   7.516 -                 if is_standard_datatype thy stds T then Const (s, T)
   7.517 -                 else funpow j (curry (op $) (suc_const T)) (zero_const T)
   7.518 +                 Const (s, T)
   7.519                 else
   7.520                   do_term depth Ts (Const (@{const_name of_int}, int_T --> T)
   7.521                                     $ Const (s, int_T))
   7.522 @@ -1732,9 +1703,9 @@
   7.523                 t
   7.524      and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
   7.525          (Abs (Name.uu, body_type T,
   7.526 -              select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
   7.527 +              select_nth_constr_arg ctxt x (Bound 0) n res_T), [])
   7.528        | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
   7.529 -        (select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
   7.530 +        (select_nth_constr_arg ctxt x (do_term depth Ts t) n res_T, ts)
   7.531      and quot_rep_of depth Ts abs_T rep_T ts =
   7.532        select_nth_constr_arg_with_args depth Ts
   7.533            (@{const_name Quot}, rep_T --> abs_T) ts 0 rep_T
   7.534 @@ -1753,7 +1724,7 @@
   7.535              else
   7.536                def_inline_threshold_for_non_booleans
   7.537            val (const, ts) =
   7.538 -            if is_built_in_const thy stds x then
   7.539 +            if is_built_in_const x then
   7.540                (Const x, ts)
   7.541              else case AList.lookup (op =) case_names s of
   7.542                SOME n =>
   7.543 @@ -1769,7 +1740,7 @@
   7.544                     drop n ts)
   7.545                  end
   7.546              | _ =>
   7.547 -              if is_constr ctxt stds x then
   7.548 +              if is_constr ctxt x then
   7.549                  (Const x, ts)
   7.550                else if is_stale_constr ctxt x then
   7.551                  raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
   7.552 @@ -1777,7 +1748,7 @@
   7.553                else if is_quot_abs_fun ctxt x then
   7.554                  case T of
   7.555                    Type (@{type_name fun}, [rep_T, abs_T as Type (abs_s, _)]) =>
   7.556 -                  if is_basic_datatype thy [(NONE, true)] abs_s then
   7.557 +                  if is_basic_datatype abs_s then
   7.558                      raise NOT_SUPPORTED ("abstraction function on " ^
   7.559                                           quote abs_s)
   7.560                    else
   7.561 @@ -1788,7 +1759,7 @@
   7.562                else if is_quot_rep_fun ctxt x then
   7.563                  case T of
   7.564                    Type (@{type_name fun}, [abs_T as Type (abs_s, _), rep_T]) =>
   7.565 -                  if is_basic_datatype thy [(NONE, true)] abs_s then
   7.566 +                  if is_basic_datatype abs_s then
   7.567                      raise NOT_SUPPORTED ("representation function on " ^
   7.568                                           quote abs_s)
   7.569                    else
   7.570 @@ -1828,7 +1799,7 @@
   7.571                  end
   7.572                else if is_rep_fun ctxt x then
   7.573                  let val x' = mate_of_rep_fun ctxt x in
   7.574 -                  if is_constr ctxt stds x' then
   7.575 +                  if is_constr ctxt x' then
   7.576                      select_nth_constr_arg_with_args depth Ts x' ts 0
   7.577                                                      (range_type T)
   7.578                    else if is_quot_type ctxt (domain_type T) then
   7.579 @@ -1993,7 +1964,7 @@
   7.580        end
   7.581      | NONE => []
   7.582    end
   7.583 -fun optimized_quot_type_axioms ctxt stds abs_z =
   7.584 +fun optimized_quot_type_axioms ctxt abs_z =
   7.585    let
   7.586      val abs_T = Type abs_z
   7.587      val rep_T = rep_type_for_quot_type ctxt abs_T
   7.588 @@ -2002,7 +1973,7 @@
   7.589      val x_var = Var (("x", 0), rep_T)
   7.590      val y_var = Var (("y", 0), rep_T)
   7.591      val x = (@{const_name Quot}, rep_T --> abs_T)
   7.592 -    val sel_a_t = select_nth_constr_arg ctxt stds x a_var 0 rep_T
   7.593 +    val sel_a_t = select_nth_constr_arg ctxt x a_var 0 rep_T
   7.594      val normal_fun =
   7.595        Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
   7.596      val normal_x = normal_fun $ x_var
   7.597 @@ -2022,7 +1993,7 @@
   7.598      |> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
   7.599    end
   7.600  
   7.601 -fun codatatype_bisim_axioms (hol_ctxt as {ctxt, stds, ...}) T =
   7.602 +fun codatatype_bisim_axioms (hol_ctxt as {ctxt, ...}) T =
   7.603    let
   7.604      val xs = datatype_constrs hol_ctxt T
   7.605      val pred_T = T --> bool_T
   7.606 @@ -2039,8 +2010,8 @@
   7.607      fun nth_sub_bisim x n nth_T =
   7.608        (if is_codatatype ctxt nth_T then bisim_const nth_T $ n_var_minus_1
   7.609         else HOLogic.eq_const nth_T)
   7.610 -      $ select_nth_constr_arg ctxt stds x x_var n nth_T
   7.611 -      $ select_nth_constr_arg ctxt stds x y_var n nth_T
   7.612 +      $ select_nth_constr_arg ctxt x x_var n nth_T
   7.613 +      $ select_nth_constr_arg ctxt x y_var n nth_T
   7.614      fun case_func (x as (_, T)) =
   7.615        let
   7.616          val arg_Ts = binder_types T
   7.617 @@ -2102,9 +2073,9 @@
   7.618                          ScnpReconstruct.sizechange_tac]
   7.619  
   7.620  fun uncached_is_well_founded_inductive_pred
   7.621 -        ({thy, ctxt, stds, debug, tac_timeout, intro_table, ...} : hol_context)
   7.622 +        ({thy, ctxt, debug, tac_timeout, intro_table, ...} : hol_context)
   7.623          (x as (_, T)) =
   7.624 -  case def_props_for_const thy stds intro_table x of
   7.625 +  case def_props_for_const thy intro_table x of
   7.626      [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
   7.627                        [Const x])
   7.628    | intro_ts =>
   7.629 @@ -2351,10 +2322,10 @@
   7.630    else
   7.631      raw_inductive_pred_axiom hol_ctxt x
   7.632  
   7.633 -fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_tables, simp_table,
   7.634 +fun equational_fun_axioms (hol_ctxt as {thy, ctxt, def_tables, simp_table,
   7.635                                          psimp_table, ...}) x =
   7.636 -  case def_props_for_const thy stds (!simp_table) x of
   7.637 -    [] => (case def_props_for_const thy stds psimp_table x of
   7.638 +  case def_props_for_const thy (!simp_table) x of
   7.639 +    [] => (case def_props_for_const thy psimp_table x of
   7.640               [] => (if is_inductive_pred hol_ctxt x then
   7.641                        [inductive_pred_axiom hol_ctxt x]
   7.642                      else case def_of_const thy def_tables x of
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 16:44:46 2014 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
     8.3 @@ -55,8 +55,7 @@
     8.4  
     8.5  fun pull x xs = x :: filter_out (curry (op =) x) xs
     8.6  
     8.7 -fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...}
     8.8 -                         : datatype_spec) = true
     8.9 +fun is_datatype_acyclic ({co = false, deep = true, ...} : datatype_spec) = true
    8.10    | is_datatype_acyclic _ = false
    8.11  
    8.12  fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
    8.13 @@ -1499,7 +1498,6 @@
    8.14    maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
    8.15         (index_seq 0 (num_sels_for_constr_type T))
    8.16  fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
    8.17 -  | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
    8.18    | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
    8.19    | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
    8.20                             {typ, constrs, ...} =
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 03 16:44:46 2014 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 03 22:33:22 2014 +0100
     9.3 @@ -356,8 +356,8 @@
     9.4    in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
     9.5  and reconstruct_term maybe_opt unfold pool
     9.6          (wacky_names as ((maybe_name, abs_name), _))
     9.7 -        (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
     9.8 -                   bits, datatypes, ofs, ...})
     9.9 +        (scope as {hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits,
    9.10 +                   datatypes, ofs, ...})
    9.11          atomss sel_names rel_table bounds =
    9.12    let
    9.13      val for_auto = (maybe_name = "")
    9.14 @@ -507,7 +507,7 @@
    9.15        | term_for_atom _ @{typ bool} _ j _ =
    9.16          if j = 0 then @{const False} else @{const True}
    9.17        | term_for_atom seen T _ j k =
    9.18 -        if T = nat_T andalso is_standard_datatype thy stds nat_T then
    9.19 +        if T = nat_T then
    9.20            HOLogic.mk_number nat_T j
    9.21          else if T = int_T then
    9.22            HOLogic.mk_number int_T (int_for_atom (k, 0) j)
    9.23 @@ -518,7 +518,7 @@
    9.24          else case datatype_spec datatypes T of
    9.25            NONE => nth_atom thy atomss pool for_auto T j
    9.26          | SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j
    9.27 -        | SOME {co, standard, constrs, ...} =>
    9.28 +        | SOME {co, constrs, ...} =>
    9.29            let
    9.30              fun tuples_for_const (s, T) =
    9.31                tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
    9.32 @@ -553,9 +553,8 @@
    9.33                map (map_filter (fn js => if hd js = real_j then SOME (tl js)
    9.34                                          else NONE)) sel_jsss
    9.35              val uncur_arg_Ts = binder_types constr_T
    9.36 -            val maybe_cyclic = co orelse not standard
    9.37            in
    9.38 -            if maybe_cyclic andalso not (null seen) andalso
    9.39 +            if co andalso not (null seen) andalso
    9.40                 member (op =) (seen |> unfold ? (fst o split_last)) (T, j) then
    9.41                cyclic_var ()
    9.42              else if constr_s = @{const_name Word} then
    9.43 @@ -564,7 +563,7 @@
    9.44                    (value_of_bits (the_single arg_jsss))
    9.45              else
    9.46                let
    9.47 -                val seen = seen |> maybe_cyclic ? cons (T, j)
    9.48 +                val seen = seen |> co ? cons (T, j)
    9.49                  val ts =
    9.50                    if length arg_Ts = 0 then
    9.51                      []
    9.52 @@ -587,16 +586,9 @@
    9.53                    else
    9.54                      list_comb (Const constr_x, ts)
    9.55                in
    9.56 -                if maybe_cyclic then
    9.57 +                if co then
    9.58                    let val var = cyclic_var () in
    9.59 -                    if unfold andalso not standard andalso
    9.60 -                       length seen = 1 andalso
    9.61 -                       exists_subterm
    9.62 -                           (fn Const (s, _) =>
    9.63 -                               String.isPrefix (cyclic_const_prefix ()) s
    9.64 -                             | t' => t' = var) t then
    9.65 -                      subst_atomic [(var, cyclic_atom ())] t
    9.66 -                    else if exists_subterm (curry (op =) var) t then
    9.67 +                    if exists_subterm (curry (op =) var) t then
    9.68                        if co then
    9.69                          Const (@{const_name The}, (T --> bool_T) --> T)
    9.70                          $ Abs (cyclic_co_val_name (), T,
    9.71 @@ -876,7 +868,7 @@
    9.72      end
    9.73  
    9.74  fun reconstruct_hol_model {show_datatypes, show_skolems, show_consts}
    9.75 -        ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
    9.76 +        ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
    9.77                        debug, whacks, binary_ints, destroy_constrs, specialize,
    9.78                        star_linear_preds, total_consts, needs, tac_timeout,
    9.79                        evals, case_names, def_tables, nondef_table, nondefs,
    9.80 @@ -892,12 +884,11 @@
    9.81        add_wacky_syntax ctxt
    9.82      val hol_ctxt =
    9.83        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
    9.84 -       stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    9.85 -       whacks = whacks, binary_ints = binary_ints,
    9.86 -       destroy_constrs = destroy_constrs, specialize = specialize,
    9.87 -       star_linear_preds = star_linear_preds, total_consts = total_consts,
    9.88 -       needs = needs, tac_timeout = tac_timeout, evals = evals,
    9.89 -       case_names = case_names, def_tables = def_tables,
    9.90 +       wfs = wfs, user_axioms = user_axioms, debug = debug, whacks = whacks,
    9.91 +       binary_ints = binary_ints, destroy_constrs = destroy_constrs,
    9.92 +       specialize = specialize, star_linear_preds = star_linear_preds,
    9.93 +       total_consts = total_consts, needs = needs, tac_timeout = tac_timeout,
    9.94 +       evals = evals, case_names = case_names, def_tables = def_tables,
    9.95         nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
    9.96         psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    9.97         intro_table = intro_table, ground_thm_table = ground_thm_table,
    9.98 @@ -960,14 +951,12 @@
    9.99                    else [Pretty.str (unrep ())]))]))
   9.100      fun integer_datatype T =
   9.101        [{typ = T, card = card_of_type card_assigns T, co = false,
   9.102 -        standard = true, self_rec = true, complete = (false, false),
   9.103 -        concrete = (true, true), deep = true, constrs = []}]
   9.104 +        self_rec = true, complete = (false, false), concrete = (true, true),
   9.105 +        deep = true, constrs = []}]
   9.106        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
   9.107      val (codatatypes, datatypes) =
   9.108        datatypes |> filter #deep |> List.partition #co
   9.109 -                ||> append (integer_datatype int_T
   9.110 -                            |> is_standard_datatype thy stds nat_T
   9.111 -                               ? append (integer_datatype nat_T))
   9.112 +                ||> append (integer_datatype nat_T @ integer_datatype int_T)
   9.113      val block_of_datatypes =
   9.114        if show_datatypes andalso not (null datatypes) then
   9.115          [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 03 16:44:46 2014 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 03 22:33:22 2014 +0100
    10.3 @@ -129,7 +129,7 @@
    10.4  fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
    10.5      could_exist_alpha_subtype alpha_T T
    10.6    | could_exist_alpha_sub_mtype ctxt alpha_T T =
    10.7 -    (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)
    10.8 +    (T = alpha_T orelse is_datatype ctxt T)
    10.9  
   10.10  fun exists_alpha_sub_mtype MAlpha = true
   10.11    | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
   10.12 @@ -737,13 +737,11 @@
   10.13                                             frame2)
   10.14    end
   10.15  
   10.16 -fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
   10.17 -                             max_fresh, ...}) =
   10.18 +fun consider_term (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, max_fresh, ...}) =
   10.19    let
   10.20      fun is_enough_eta_expanded t =
   10.21        case strip_comb t of
   10.22 -        (Const x, ts) => the_default 0 (arity_of_built_in_const thy stds x)
   10.23 -        <= length ts
   10.24 +        (Const x, ts) => the_default 0 (arity_of_built_in_const x) <= length ts
   10.25        | _ => true
   10.26      val mtype_for = fresh_mtype_for_type mdata false
   10.27      fun mtype_for_set x T = MFun (mtype_for (pseudo_domain_type T), V x, bool_M)
   10.28 @@ -894,9 +892,9 @@
   10.29                  do_fragile_set_operation T accum
   10.30                else if is_sel s then
   10.31                  (mtype_for_sel mdata x, accum)
   10.32 -              else if is_constr ctxt stds x then
   10.33 +              else if is_constr ctxt x then
   10.34                  (mtype_for_constr mdata x, accum)
   10.35 -              else if is_built_in_const thy stds x then
   10.36 +              else if is_built_in_const x then
   10.37                  (fresh_mtype_for_type mdata true T, accum)
   10.38                else
   10.39                  let val M = mtype_for T in
   10.40 @@ -1074,20 +1072,20 @@
   10.41    [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
   10.42  val bounteous_consts = [@{const_name bisim}]
   10.43  
   10.44 -fun is_harmless_axiom ({hol_ctxt = {thy, stds, ...}, ...} : mdata) t =
   10.45 -    Term.add_consts t []
   10.46 -    |> filter_out (is_built_in_const thy stds)
   10.47 -    |> (forall (member (op =) harmless_consts o original_name o fst) orf
   10.48 -        exists (member (op =) bounteous_consts o fst))
   10.49 +fun is_harmless_axiom t =
   10.50 +  Term.add_consts t []
   10.51 +  |> filter_out is_built_in_const
   10.52 +  |> (forall (member (op =) harmless_consts o original_name o fst) orf
   10.53 +      exists (member (op =) bounteous_consts o fst))
   10.54  
   10.55  fun consider_nondefinitional_axiom mdata t =
   10.56 -  if is_harmless_axiom mdata t then I
   10.57 +  if is_harmless_axiom t then I
   10.58    else consider_general_formula mdata Plus t
   10.59  
   10.60  fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...} : mdata) t =
   10.61    if not (is_constr_pattern_formula ctxt t) then
   10.62      consider_nondefinitional_axiom mdata t
   10.63 -  else if is_harmless_axiom mdata t then
   10.64 +  else if is_harmless_axiom t then
   10.65      I
   10.66    else
   10.67      let
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 03 16:44:46 2014 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 03 22:33:22 2014 +0100
    11.3 @@ -418,7 +418,7 @@
    11.4      maps factorize [mk_fst z, mk_snd z]
    11.5    | factorize z = [z]
    11.6  
    11.7 -fun nut_from_term (hol_ctxt as {thy, ctxt, stds, ...}) eq =
    11.8 +fun nut_from_term (hol_ctxt as {ctxt, ...}) eq =
    11.9    let
   11.10      fun aux eq ss Ts t =
   11.11        let
   11.12 @@ -525,8 +525,8 @@
   11.13          | (Const (@{const_name relcomp}, T), [t1, t2]) =>
   11.14            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   11.15          | (Const (x as (s as @{const_name Suc}, T)), []) =>
   11.16 -          if is_built_in_const thy stds x then Cst (Suc, T, Any)
   11.17 -          else if is_constr ctxt stds x then do_construct x []
   11.18 +          if is_built_in_const x then Cst (Suc, T, Any)
   11.19 +          else if is_constr ctxt x then do_construct x []
   11.20            else ConstName (s, T, Any)
   11.21          | (Const (@{const_name finite}, T), [t1]) =>
   11.22            (if is_finite_type hol_ctxt (domain_type T) then
   11.23 @@ -536,27 +536,27 @@
   11.24             | _ => Op1 (Finite, bool_T, Any, sub t1))
   11.25          | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
   11.26          | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
   11.27 -          if is_built_in_const thy stds x then Cst (Num 0, T, Any)
   11.28 -          else if is_constr ctxt stds x then do_construct x []
   11.29 +          if is_built_in_const x then Cst (Num 0, T, Any)
   11.30 +          else if is_constr ctxt x then do_construct x []
   11.31            else ConstName (s, T, Any)
   11.32          | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
   11.33 -          if is_built_in_const thy stds x then Cst (Num 1, T, Any)
   11.34 +          if is_built_in_const x then Cst (Num 1, T, Any)
   11.35            else ConstName (s, T, Any)
   11.36          | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
   11.37 -          if is_built_in_const thy stds x then Cst (Add, T, Any)
   11.38 +          if is_built_in_const x then Cst (Add, T, Any)
   11.39            else ConstName (s, T, Any)
   11.40          | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
   11.41 -          if is_built_in_const thy stds x then Cst (Subtract, T, Any)
   11.42 +          if is_built_in_const x then Cst (Subtract, T, Any)
   11.43            else ConstName (s, T, Any)
   11.44          | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
   11.45 -          if is_built_in_const thy stds x then Cst (Multiply, T, Any)
   11.46 +          if is_built_in_const x then Cst (Multiply, T, Any)
   11.47            else ConstName (s, T, Any)
   11.48          | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
   11.49 -          if is_built_in_const thy stds x then Cst (Divide, T, Any)
   11.50 +          if is_built_in_const x then Cst (Divide, T, Any)
   11.51            else ConstName (s, T, Any)
   11.52          | (t0 as Const (x as (@{const_name ord_class.less}, _)),
   11.53             ts as [t1, t2]) =>
   11.54 -          if is_built_in_const thy stds x then
   11.55 +          if is_built_in_const x then
   11.56              Op2 (Less, bool_T, Any, sub t1, sub t2)
   11.57            else
   11.58              do_apply t0 ts
   11.59 @@ -564,7 +564,7 @@
   11.60             ts as [t1, t2]) =>
   11.61            if is_set_like_type (domain_type T) then
   11.62              Op2 (Subset, bool_T, Any, sub t1, sub t2)
   11.63 -          else if is_built_in_const thy stds x then
   11.64 +          else if is_built_in_const x then
   11.65              (* FIXME: find out if this case is necessary *)
   11.66              Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
   11.67            else
   11.68 @@ -572,7 +572,7 @@
   11.69          | (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any)
   11.70          | (Const (@{const_name Nitpick.nat_lcm}, T), []) => Cst (Lcm, T, Any)
   11.71          | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
   11.72 -          if is_built_in_const thy stds x then
   11.73 +          if is_built_in_const x then
   11.74              let val num_T = domain_type T in
   11.75                Op2 (Apply, num_T --> num_T, Any,
   11.76                     Cst (Subtract, num_T --> num_T --> num_T, Any),
   11.77 @@ -595,12 +595,12 @@
   11.78                    T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
   11.79            Cst (NatToInt, T, Any)
   11.80          | (t0 as Const (x as (s, T)), ts) =>
   11.81 -          if is_constr ctxt stds x then
   11.82 +          if is_constr ctxt x then
   11.83              do_construct x ts
   11.84            else if String.isPrefix numeral_prefix s then
   11.85              Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
   11.86            else
   11.87 -            (case arity_of_built_in_const thy stds x of
   11.88 +            (case arity_of_built_in_const x of
   11.89                 SOME n =>
   11.90                 (case n - length ts of
   11.91                    0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Mar 03 16:44:46 2014 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Mar 03 22:33:22 2014 +0100
    12.3 @@ -70,13 +70,11 @@
    12.4  
    12.5  fun add_to_uncurry_table ctxt t =
    12.6    let
    12.7 -    val thy = Proof_Context.theory_of ctxt
    12.8      fun aux (t1 $ t2) args table =
    12.9          let val table = aux t2 [] table in aux t1 (t2 :: args) table end
   12.10        | aux (Abs (_, _, t')) _ table = aux t' [] table
   12.11        | aux (t as Const (x as (s, _))) args table =
   12.12 -        if is_built_in_const thy [(NONE, true)] x orelse
   12.13 -           is_constr_like ctxt x orelse
   12.14 +        if is_built_in_const x orelse is_constr_like ctxt x orelse
   12.15             is_sel s orelse s = @{const_name Sigma} then
   12.16            table
   12.17          else
   12.18 @@ -126,7 +124,7 @@
   12.19  
   12.20  (** Boxing **)
   12.21  
   12.22 -fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, ...}) def orig_t =
   12.23 +fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, ...}) def orig_t =
   12.24    let
   12.25      fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
   12.26          Type (@{type_name fun}, map box_relational_operator_type Ts)
   12.27 @@ -229,7 +227,7 @@
   12.28                        let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
   12.29                          T' --> T'
   12.30                        end
   12.31 -                    else if is_built_in_const thy stds x orelse
   12.32 +                    else if is_built_in_const x orelse
   12.33                              s = @{const_name Sigma} then
   12.34                        T
   12.35                      else if is_constr_like ctxt x then
   12.36 @@ -251,7 +249,7 @@
   12.37            s_betapply new_Ts (if s1 = @{type_name fun} then
   12.38                                 t1
   12.39                               else
   12.40 -                               select_nth_constr_arg ctxt stds
   12.41 +                               select_nth_constr_arg ctxt
   12.42                                     (@{const_name FunBox},
   12.43                                      Type (@{type_name fun}, Ts1) --> T1) t1 0
   12.44                                     (Type (@{type_name fun}, Ts1)), t2)
   12.45 @@ -268,7 +266,7 @@
   12.46            s_betapply new_Ts (if s1 = @{type_name fun} then
   12.47                                 t1
   12.48                               else
   12.49 -                               select_nth_constr_arg ctxt stds
   12.50 +                               select_nth_constr_arg ctxt
   12.51                                     (@{const_name FunBox},
   12.52                                      Type (@{type_name fun}, Ts1) --> T1) t1 0
   12.53                                     (Type (@{type_name fun}, Ts1)), t2)
   12.54 @@ -306,12 +304,12 @@
   12.55        | aux _ = true
   12.56    in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
   12.57  
   12.58 -fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level t
   12.59 -                         args seen =
   12.60 +fun pull_out_constr_comb ({ctxt, ...} : hol_context) Ts relax k level t args
   12.61 +                         seen =
   12.62    let val t_comb = list_comb (t, args) in
   12.63      case t of
   12.64        Const x =>
   12.65 -      if not relax andalso is_constr ctxt stds x andalso
   12.66 +      if not relax andalso is_constr ctxt x andalso
   12.67           not (is_fun_or_set_type (fastype_of1 (Ts, t_comb))) andalso
   12.68           has_heavy_bounds_or_vars Ts t_comb andalso
   12.69           not (loose_bvar (t_comb, level)) then
   12.70 @@ -398,7 +396,7 @@
   12.71            (list_comb (t, args), seen)
   12.72    in aux [] 0 t [] [] |> fst end
   12.73  
   12.74 -fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom strong t =
   12.75 +fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, ...}) axiom strong t =
   12.76    let
   12.77      val num_occs_of_var =
   12.78        fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
   12.79 @@ -434,7 +432,7 @@
   12.80              val n = length arg_Ts
   12.81            in
   12.82              if length args = n andalso
   12.83 -               (is_constr ctxt stds x orelse s = @{const_name Pair} orelse
   12.84 +               (is_constr ctxt x orelse s = @{const_name Pair} orelse
   12.85                  x = (@{const_name Suc}, nat_T --> nat_T)) andalso
   12.86                 (not careful orelse not (is_Var t1) orelse
   12.87                  String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
   12.88 @@ -451,8 +449,7 @@
   12.89        handle SAME () => if pass1 then aux_eq Ts careful false t0 t2 t1
   12.90                          else t0 $ aux Ts false t2 $ aux Ts false t1
   12.91      and sel_eq Ts x t n nth_T nth_t =
   12.92 -      HOLogic.eq_const nth_T $ nth_t
   12.93 -                             $ select_nth_constr_arg ctxt stds x t n nth_T
   12.94 +      HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg ctxt x t n nth_T
   12.95        |> aux Ts false
   12.96    in aux [] axiom t end
   12.97  
   12.98 @@ -487,7 +484,7 @@
   12.99          aux (t1 :: prems) (Term.add_vars t1 zs) t2
  12.100    in aux [] [] end
  12.101  
  12.102 -fun find_bound_assign ctxt stds j =
  12.103 +fun find_bound_assign ctxt j =
  12.104    let
  12.105      fun do_term _ [] = NONE
  12.106        | do_term seen (t :: ts) =
  12.107 @@ -500,7 +497,7 @@
  12.108               | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
  12.109                 if j' = j andalso
  12.110                    s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
  12.111 -                 SOME (construct_value ctxt stds
  12.112 +                 SOME (construct_value ctxt
  12.113                                         (@{const_name FunBox}, T2 --> T1) [t2],
  12.114                         ts @ seen)
  12.115                 else
  12.116 @@ -527,11 +524,11 @@
  12.117        | aux _ = raise SAME ()
  12.118    in aux (t, j) handle SAME () => t end
  12.119  
  12.120 -fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) =
  12.121 +fun destroy_existential_equalities ({ctxt, ...} : hol_context) =
  12.122    let
  12.123      fun kill [] [] ts = foldr1 s_conj ts
  12.124        | kill (s :: ss) (T :: Ts) ts =
  12.125 -        (case find_bound_assign ctxt stds (length ss) [] ts of
  12.126 +        (case find_bound_assign ctxt (length ss) [] ts of
  12.127             SOME (_, []) => @{const True}
  12.128           | SOME (arg_t, ts) =>
  12.129             kill ss Ts (map (subst_one_bound (length ss)
  12.130 @@ -731,7 +728,7 @@
  12.131    forall (op aconv) (ts1 ~~ ts2)
  12.132  
  12.133  fun specialize_consts_in_term
  12.134 -        (hol_ctxt as {ctxt, thy, stds, specialize, def_tables, simp_table,
  12.135 +        (hol_ctxt as {ctxt, thy, specialize, def_tables, simp_table,
  12.136                        special_funs, ...}) def depth t =
  12.137    if not specialize orelse depth > special_max_depth then
  12.138      t
  12.139 @@ -742,11 +739,11 @@
  12.140        fun aux args Ts (Const (x as (s, T))) =
  12.141            ((if not (member (op =) blacklist x) andalso not (null args) andalso
  12.142                 not (String.isPrefix special_prefix s) andalso
  12.143 -               not (is_built_in_const thy stds x) andalso
  12.144 +               not (is_built_in_const x) andalso
  12.145                 (is_equational_fun_but_no_plain_def hol_ctxt x orelse
  12.146                  (is_some (def_of_const thy def_tables x) andalso
  12.147                   not (is_of_class_const thy x) andalso
  12.148 -                 not (is_constr ctxt stds x) andalso
  12.149 +                 not (is_constr ctxt x) andalso
  12.150                   not (is_choice_spec_fun hol_ctxt x))) then
  12.151                let
  12.152                  val eligible_args =
  12.153 @@ -895,9 +892,9 @@
  12.154  val axioms_max_depth = 255
  12.155  
  12.156  fun axioms_for_term
  12.157 -        (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
  12.158 -                      evals, def_tables, nondef_table, choice_spec_table,
  12.159 -                      nondefs, ...}) assm_ts neg_t =
  12.160 +        (hol_ctxt as {thy, ctxt, max_bisim_depth, user_axioms, evals,
  12.161 +                      def_tables, nondef_table, choice_spec_table, nondefs,
  12.162 +                      ...}) assm_ts neg_t =
  12.163    let
  12.164      val (def_assm_ts, nondef_assm_ts) =
  12.165        List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
  12.166 @@ -928,7 +925,7 @@
  12.167        case t of
  12.168          t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
  12.169        | Const (x as (s, T)) =>
  12.170 -        (if member (op aconv) seen t orelse is_built_in_const thy stds x then
  12.171 +        (if member (op aconv) seen t orelse is_built_in_const x then
  12.172             accum
  12.173           else
  12.174             let val accum = (t :: seen, axs) in
  12.175 @@ -949,7 +946,7 @@
  12.176                   fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
  12.177                        accum
  12.178                 end
  12.179 -             else if is_constr ctxt stds x then
  12.180 +             else if is_constr ctxt x then
  12.181                 accum
  12.182               else if is_descr (original_name s) then
  12.183                 fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)
  12.184 @@ -1017,8 +1014,7 @@
  12.185          #> (if is_pure_typedef ctxt T then
  12.186                fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z)
  12.187              else if is_quot_type ctxt T then
  12.188 -              fold (add_def_axiom depth)
  12.189 -                   (optimized_quot_type_axioms ctxt stds z)
  12.190 +              fold (add_def_axiom depth) (optimized_quot_type_axioms ctxt z)
  12.191              else if max_bisim_depth >= 0 andalso is_codatatype ctxt T then
  12.192                fold (add_maybe_def_axiom depth)
  12.193                     (codatatype_bisim_axioms hol_ctxt T)
  12.194 @@ -1253,8 +1249,8 @@
  12.195  val max_skolem_depth = 3
  12.196  
  12.197  fun preprocess_formulas
  12.198 -        (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
  12.199 -                      needs, ...}) assm_ts neg_t =
  12.200 +        (hol_ctxt as {ctxt, binary_ints, destroy_constrs, boxes, needs, ...})
  12.201 +        assm_ts neg_t =
  12.202    let
  12.203      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
  12.204        neg_t |> unfold_defs_in_term hol_ctxt
  12.205 @@ -1263,7 +1259,6 @@
  12.206              |> specialize_consts_in_term hol_ctxt false 0
  12.207              |> axioms_for_term hol_ctxt assm_ts
  12.208      val binarize =
  12.209 -      is_standard_datatype thy stds nat_T andalso
  12.210        case binary_ints of
  12.211          SOME false => false
  12.212        | _ => forall (may_use_binary_ints false) nondef_ts andalso
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 03 16:44:46 2014 +0100
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 03 22:33:22 2014 +0100
    13.3 @@ -22,7 +22,6 @@
    13.4      {typ: typ,
    13.5       card: int,
    13.6       co: bool,
    13.7 -     standard: bool,
    13.8       self_rec: bool,
    13.9       complete: bool * bool,
   13.10       concrete: bool * bool,
   13.11 @@ -76,7 +75,6 @@
   13.12    {typ: typ,
   13.13     card: int,
   13.14     co: bool,
   13.15 -   standard: bool,
   13.16     self_rec: bool,
   13.17     complete: bool * bool,
   13.18     concrete: bool * bool,
   13.19 @@ -142,7 +140,7 @@
   13.20     handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
   13.21  
   13.22  fun quintuple_for_scope code_type code_term code_string
   13.23 -        ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
   13.24 +        ({hol_ctxt = {ctxt, ...}, card_assigns, bits, bisim_depth,
   13.25           datatypes, ...} : scope) =
   13.26    let
   13.27      val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
   13.28 @@ -152,7 +150,7 @@
   13.29                     |> List.partition (is_fp_iterator_type o fst)
   13.30      val (secondary_card_assigns, primary_card_assigns) =
   13.31        card_assigns
   13.32 -      |> List.partition ((is_integer_type orf is_datatype ctxt stds) o fst)
   13.33 +      |> List.partition ((is_integer_type orf is_datatype ctxt) o fst)
   13.34      val cards =
   13.35        map (fn (T, k) =>
   13.36                [code_type ctxt T, code_string (" = " ^ string_of_int k)])
   13.37 @@ -433,13 +431,12 @@
   13.38                 card_assigns T
   13.39    end
   13.40  
   13.41 -fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ctxt, stds, ...})
   13.42 +fun datatype_spec_from_scope_descriptor (hol_ctxt as {ctxt, ...})
   13.43          binarize deep_dataTs finitizable_dataTs (desc as (card_assigns, _))
   13.44          (T, card) =
   13.45    let
   13.46      val deep = member (op =) deep_dataTs T
   13.47      val co = is_codatatype ctxt T
   13.48 -    val standard = is_standard_datatype thy stds T
   13.49      val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
   13.50      val self_recs = map (is_self_recursive_constr_type o snd) xs
   13.51      val (num_self_recs, num_non_self_recs) =
   13.52 @@ -459,21 +456,21 @@
   13.53      fun sum_dom_cards max =
   13.54        map (domain_card max card_assigns o snd) xs |> Integer.sum
   13.55      val constrs =
   13.56 -      fold_rev (add_constr_spec desc (not co andalso standard) card
   13.57 -                                sum_dom_cards num_self_recs num_non_self_recs)
   13.58 +      fold_rev (add_constr_spec desc (not co) card sum_dom_cards num_self_recs
   13.59 +                                num_non_self_recs)
   13.60                 (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
   13.61    in
   13.62 -    {typ = T, card = card, co = co, standard = standard, self_rec = self_rec,
   13.63 -     complete = complete, concrete = concrete, deep = deep, constrs = constrs}
   13.64 +    {typ = T, card = card, co = co, self_rec = self_rec, complete = complete,
   13.65 +     concrete = concrete, deep = deep, constrs = constrs}
   13.66    end
   13.67  
   13.68 -fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
   13.69 +fun scope_from_descriptor (hol_ctxt as {ctxt, ...}) binarize deep_dataTs
   13.70                            finitizable_dataTs (desc as (card_assigns, _)) =
   13.71    let
   13.72      val datatypes =
   13.73        map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
   13.74                                                 finitizable_dataTs desc)
   13.75 -          (filter (is_datatype ctxt stds o fst) card_assigns)
   13.76 +          (filter (is_datatype ctxt o fst) card_assigns)
   13.77      val bits = card_of_type card_assigns @{typ signed_bit} - 1
   13.78                 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   13.79                        card_of_type card_assigns @{typ unsigned_bit}