remove "fast_descs" option from Nitpick;
authorblanchet
Tue Sep 14 13:24:18 2010 +0200 (2010-09-14)
changeset 393596f49c7fbb1b1
parent 39358 6bc2f7971df0
child 39360 cdf2c3341422
remove "fast_descs" option from Nitpick;
the option has been unsound for over a year and is too imprecise to be of any use when made sound
doc-src/Nitpick/nitpick.tex
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.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
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Sep 14 12:52:50 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Sep 14 13:24:18 2010 +0200
     1.3 @@ -296,40 +296,18 @@
     1.4  \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
     1.5  \hbox{}\qquad\qquad $x = a_3$ \\
     1.6  \hbox{}\qquad Constant: \nopagebreak \\
     1.7 -\hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$
     1.8 +\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
     1.9  \postw
    1.10  
    1.11 -We can see more clearly now. Since the predicate $P$ isn't true for a unique
    1.12 -value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even
    1.13 -$a_1$. Since $P~a_1$ is false, the entire formula is falsified.
    1.14 -
    1.15 -As an optimization, Nitpick's preprocessor introduced the special constant
    1.16 -``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e.,
    1.17 -$\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$
    1.18 -satisfying $P~y$. We disable this optimization by passing the
    1.19 -\textit{full\_descrs} option:
    1.20 +As the result of an optimization, Nitpick directly assigned a value to the
    1.21 +subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
    1.22 +disable this optimization by using the command
    1.23  
    1.24  \prew
    1.25 -\textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount]
    1.26 -\slshape
    1.27 -Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
    1.28 -\hbox{}\qquad Free variables: \nopagebreak \\
    1.29 -\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
    1.30 -\hbox{}\qquad\qquad $x = a_3$ \\
    1.31 -\hbox{}\qquad Constant: \nopagebreak \\
    1.32 -\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
    1.33 +\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}]
    1.34  \postw
    1.35  
    1.36 -As the result of another optimization, Nitpick directly assigned a value to the
    1.37 -subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
    1.38 -disable this second optimization by using the command
    1.39 -
    1.40 -\prew
    1.41 -\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\,
    1.42 -\textit{show\_consts}]
    1.43 -\postw
    1.44 -
    1.45 -we finally get \textit{The}:
    1.46 +we get \textit{The}:
    1.47  
    1.48  \prew
    1.49  \slshape Constant: \nopagebreak \\
    1.50 @@ -2490,13 +2468,6 @@
    1.51  {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
    1.52  (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
    1.53  
    1.54 -\optrue{fast\_descrs}{full\_descrs}
    1.55 -Specifies whether Nitpick should optimize the definite and indefinite
    1.56 -description operators (THE and SOME). The optimized versions usually help
    1.57 -Nitpick generate more counterexamples or at least find them faster, but only the
    1.58 -unoptimized versions are complete when all types occurring in the formula are
    1.59 -finite.
    1.60 -
    1.61  {\small See also \textit{debug} (\S\ref{output-format}).}
    1.62  
    1.63  \opnodefault{whack}{term\_list}
     2.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Sep 14 12:52:50 2010 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Sep 14 13:24:18 2010 +0200
     2.3 @@ -892,7 +892,7 @@
     2.4  nitpick [expect = none]
     2.5  sorry
     2.6  
     2.7 -nitpick_params [full_descrs, max_potential = 1]
     2.8 +nitpick_params [max_potential = 1]
     2.9  
    2.10  lemma "(THE j. j > Suc 2 \<and> j \<le> 3) \<noteq> 0"
    2.11  nitpick [card nat = 2, expect = potential]
    2.12 @@ -940,7 +940,7 @@
    2.13  nitpick [card nat = 6, expect = none]
    2.14  sorry
    2.15  
    2.16 -nitpick_params [fast_descrs, max_potential = 0]
    2.17 +nitpick_params [max_potential = 0]
    2.18  
    2.19  subsection {* Destructors and Recursors *}
    2.20  
     3.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Sep 14 12:52:50 2010 +0200
     3.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Sep 14 13:24:18 2010 +0200
     3.3 @@ -21,8 +21,8 @@
     3.4    {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
     3.5     stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
     3.6     whacks = [], binary_ints = SOME false, destroy_constrs = false,
     3.7 -   specialize = false, star_linear_preds = false, fast_descrs = false,
     3.8 -   tac_timeout = NONE, evals = [], case_names = [], def_table = def_table,
     3.9 +   specialize = false, star_linear_preds = false, tac_timeout = NONE,
    3.10 +   evals = [], case_names = [], def_table = def_table,
    3.11     nondef_table = Symtab.empty, user_nondefs = [],
    3.12     simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
    3.13     choice_spec_table = Symtab.empty, intro_table = Symtab.empty,
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 14 12:52:50 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 14 13:24:18 2010 +0200
     4.3 @@ -34,7 +34,6 @@
     4.4       destroy_constrs: bool,
     4.5       specialize: bool,
     4.6       star_linear_preds: bool,
     4.7 -     fast_descrs: bool,
     4.8       peephole_optim: bool,
     4.9       datatype_sym_break: int,
    4.10       kodkod_sym_break: int,
    4.11 @@ -108,7 +107,6 @@
    4.12     destroy_constrs: bool,
    4.13     specialize: bool,
    4.14     star_linear_preds: bool,
    4.15 -   fast_descrs: bool,
    4.16     peephole_optim: bool,
    4.17     datatype_sym_break: int,
    4.18     kodkod_sym_break: int,
    4.19 @@ -207,10 +205,10 @@
    4.20           boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    4.21           verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
    4.22           binary_ints, destroy_constrs, specialize, star_linear_preds,
    4.23 -         fast_descrs, peephole_optim, datatype_sym_break, kodkod_sym_break,
    4.24 -         tac_timeout, max_threads, show_datatypes, show_consts, evals, formats,
    4.25 -         atomss, max_potential, max_genuine, check_potential, check_genuine,
    4.26 -         batch_size, ...} = params
    4.27 +         peephole_optim, datatype_sym_break, kodkod_sym_break, tac_timeout,
    4.28 +         max_threads, show_datatypes, show_consts, evals, formats, atomss,
    4.29 +         max_potential, max_genuine, check_potential, check_genuine, batch_size,
    4.30 +         ...} = params
    4.31      val state_ref = Unsynchronized.ref state
    4.32      val pprint =
    4.33        if auto then
    4.34 @@ -280,14 +278,13 @@
    4.35         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    4.36         whacks = whacks, binary_ints = binary_ints,
    4.37         destroy_constrs = destroy_constrs, specialize = specialize,
    4.38 -       star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
    4.39 -       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
    4.40 -       def_table = def_table, nondef_table = nondef_table,
    4.41 -       user_nondefs = user_nondefs, simp_table = simp_table,
    4.42 -       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    4.43 -       intro_table = intro_table, ground_thm_table = ground_thm_table,
    4.44 -       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
    4.45 -       special_funs = Unsynchronized.ref [],
    4.46 +       star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
    4.47 +       evals = evals, case_names = case_names, def_table = def_table,
    4.48 +       nondef_table = nondef_table, user_nondefs = user_nondefs,
    4.49 +       simp_table = simp_table, psimp_table = psimp_table,
    4.50 +       choice_spec_table = choice_spec_table, intro_table = intro_table,
    4.51 +       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    4.52 +       skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    4.53         unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    4.54         constr_cache = Unsynchronized.ref []}
    4.55      val pseudo_frees = fold Term.add_frees assm_ts []
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Sep 14 12:52:50 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Sep 14 13:24:18 2010 +0200
     5.3 @@ -27,7 +27,6 @@
     5.4       destroy_constrs: bool,
     5.5       specialize: bool,
     5.6       star_linear_preds: bool,
     5.7 -     fast_descrs: bool,
     5.8       tac_timeout: Time.time option,
     5.9       evals: term list,
    5.10       case_names: (string * int) list,
    5.11 @@ -181,9 +180,9 @@
    5.12    val all_axioms_of :
    5.13      Proof.context -> (term * term) list -> term list * term list * term list
    5.14    val arity_of_built_in_const :
    5.15 -    theory -> (typ option * bool) list -> bool -> styp -> int option
    5.16 +    theory -> (typ option * bool) list -> styp -> int option
    5.17    val is_built_in_const :
    5.18 -    theory -> (typ option * bool) list -> bool -> styp -> bool
    5.19 +    theory -> (typ option * bool) list -> styp -> bool
    5.20    val term_under_def : term -> term
    5.21    val case_const_names :
    5.22      Proof.context -> (typ option * bool) list -> (string * int) list
    5.23 @@ -254,7 +253,6 @@
    5.24     destroy_constrs: bool,
    5.25     specialize: bool,
    5.26     star_linear_preds: bool,
    5.27 -   fast_descrs: bool,
    5.28     tac_timeout: Time.time option,
    5.29     evals: term list,
    5.30     case_names: (string * int) list,
    5.31 @@ -434,9 +432,6 @@
    5.32     (@{const_name nat}, 0),
    5.33     (@{const_name nat_gcd}, 0),
    5.34     (@{const_name nat_lcm}, 0)]
    5.35 -val built_in_descr_consts =
    5.36 -  [(@{const_name The}, 1),
    5.37 -   (@{const_name Eps}, 1)]
    5.38  val built_in_typed_consts =
    5.39    [((@{const_name zero_class.zero}, int_T), 0),
    5.40     ((@{const_name one_class.one}, int_T), 0),
    5.41 @@ -1317,15 +1312,14 @@
    5.42        user_defs @ built_in_defs
    5.43    in (defs, built_in_nondefs, user_nondefs) end
    5.44  
    5.45 -fun arity_of_built_in_const thy stds fast_descrs (s, T) =
    5.46 +fun arity_of_built_in_const thy stds (s, T) =
    5.47    if s = @{const_name If} then
    5.48      if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
    5.49    else
    5.50      let val std_nats = is_standard_datatype thy stds nat_T in
    5.51        case AList.lookup (op =)
    5.52                      (built_in_consts
    5.53 -                     |> std_nats ? append built_in_nat_consts
    5.54 -                     |> fast_descrs ? append built_in_descr_consts) s of
    5.55 +                     |> std_nats ? append built_in_nat_consts) s of
    5.56          SOME n => SOME n
    5.57        | NONE =>
    5.58          case AList.lookup (op =)
    5.59 @@ -1344,7 +1338,7 @@
    5.60                   else
    5.61                     NONE
    5.62      end
    5.63 -val is_built_in_const = is_some oooo arity_of_built_in_const
    5.64 +val is_built_in_const = is_some ooo arity_of_built_in_const
    5.65  
    5.66  (* This function is designed to work for both real definition axioms and
    5.67     simplification rules (equational specifications). *)
    5.68 @@ -1361,8 +1355,8 @@
    5.69  (* Here we crucially rely on "specialize_type" performing a preorder traversal
    5.70     of the term, without which the wrong occurrence of a constant could be
    5.71     matched in the face of overloading. *)
    5.72 -fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
    5.73 -  if is_built_in_const thy stds fast_descrs x then
    5.74 +fun def_props_for_const thy stds table (x as (s, _)) =
    5.75 +  if is_built_in_const thy stds x then
    5.76      []
    5.77    else
    5.78      these (Symtab.lookup table s)
    5.79 @@ -1384,12 +1378,11 @@
    5.80    in fold_rev aux args (SOME rhs) end
    5.81  
    5.82  fun def_of_const thy table (x as (s, _)) =
    5.83 -  if is_built_in_const thy [(NONE, false)] false x orelse
    5.84 +  if is_built_in_const thy [(NONE, false)] x orelse
    5.85       original_name s <> s then
    5.86      NONE
    5.87    else
    5.88 -    x |> def_props_for_const thy [(NONE, false)] false table
    5.89 -      |> List.last
    5.90 +    x |> def_props_for_const thy [(NONE, false)] table |> List.last
    5.91        |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
    5.92      handle List.Empty => NONE
    5.93  
    5.94 @@ -1438,16 +1431,14 @@
    5.95    end
    5.96  
    5.97  fun fixpoint_kind_of_const thy table x =
    5.98 -  if is_built_in_const thy [(NONE, false)] false x then
    5.99 -    NoFp
   5.100 -  else
   5.101 -    fixpoint_kind_of_rhs (the (def_of_const thy table x))
   5.102 -    handle Option.Option => NoFp
   5.103 +  if is_built_in_const thy [(NONE, false)] x then NoFp
   5.104 +  else fixpoint_kind_of_rhs (the (def_of_const thy table x))
   5.105 +  handle Option.Option => NoFp
   5.106  
   5.107 -fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
   5.108 -                             ...} : hol_context) x =
   5.109 +fun is_real_inductive_pred ({thy, stds, def_table, intro_table, ...}
   5.110 +                            : hol_context) x =
   5.111    fixpoint_kind_of_const thy def_table x <> NoFp andalso
   5.112 -  not (null (def_props_for_const thy stds fast_descrs intro_table x))
   5.113 +  not (null (def_props_for_const thy stds intro_table x))
   5.114  fun is_inductive_pred hol_ctxt (x as (s, _)) =
   5.115    is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
   5.116    String.isPrefix lbfp_prefix s
   5.117 @@ -1532,10 +1523,9 @@
   5.118                      exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
   5.119                  choice_spec_table
   5.120  
   5.121 -fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
   5.122 -                             ...} : hol_context) x =
   5.123 -  exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
   5.124 -                                                     x)))
   5.125 +fun is_real_equational_fun ({thy, stds, simp_table, psimp_table, ...}
   5.126 +                            : hol_context) x =
   5.127 +  exists (fn table => not (null (def_props_for_const thy stds table x)))
   5.128           [!simp_table, psimp_table]
   5.129  fun is_equational_fun_but_no_plain_def hol_ctxt =
   5.130    is_real_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt
   5.131 @@ -1625,8 +1615,8 @@
   5.132  val def_inline_threshold_for_non_booleans = 20
   5.133  
   5.134  fun unfold_defs_in_term
   5.135 -        (hol_ctxt as {thy, ctxt, stds, whacks, fast_descrs, case_names,
   5.136 -                      def_table, ground_thm_table, ersatz_table, ...}) =
   5.137 +        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_table,
   5.138 +                      ground_thm_table, ersatz_table, ...}) =
   5.139    let
   5.140      fun do_term depth Ts t =
   5.141        case t of
   5.142 @@ -1702,7 +1692,7 @@
   5.143              else
   5.144                def_inline_threshold_for_non_booleans
   5.145            val (const, ts) =
   5.146 -            if is_built_in_const thy stds fast_descrs x then
   5.147 +            if is_built_in_const thy stds x then
   5.148                (Const x, ts)
   5.149              else case AList.lookup (op =) case_names s of
   5.150                SOME n =>
   5.151 @@ -2046,9 +2036,9 @@
   5.152                          ScnpReconstruct.sizechange_tac]
   5.153  
   5.154  fun uncached_is_well_founded_inductive_pred
   5.155 -        ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
   5.156 -         : hol_context) (x as (_, T)) =
   5.157 -  case def_props_for_const thy stds fast_descrs intro_table x of
   5.158 +        ({thy, ctxt, stds, debug, tac_timeout, intro_table, ...} : hol_context)
   5.159 +        (x as (_, T)) =
   5.160 +  case def_props_for_const thy stds intro_table x of
   5.161      [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
   5.162                        [Const x])
   5.163    | intro_ts =>
   5.164 @@ -2281,10 +2271,10 @@
   5.165    else
   5.166      raw_inductive_pred_axiom hol_ctxt x
   5.167  
   5.168 -fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, fast_descrs, def_table,
   5.169 -                                        simp_table, psimp_table, ...}) x =
   5.170 -  case def_props_for_const thy stds fast_descrs (!simp_table) x of
   5.171 -    [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
   5.172 +fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_table, simp_table,
   5.173 +                                        psimp_table, ...}) x =
   5.174 +  case def_props_for_const thy stds (!simp_table) x of
   5.175 +    [] => (case def_props_for_const thy stds psimp_table x of
   5.176               [] => (if is_inductive_pred hol_ctxt x then
   5.177                        [inductive_pred_axiom hol_ctxt x]
   5.178                      else case def_of_const thy def_table x of
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Sep 14 12:52:50 2010 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Sep 14 13:24:18 2010 +0200
     6.3 @@ -58,7 +58,6 @@
     6.4     ("destroy_constrs", "true"),
     6.5     ("specialize", "true"),
     6.6     ("star_linear_preds", "true"),
     6.7 -   ("fast_descrs", "true"),
     6.8     ("peephole_optim", "true"),
     6.9     ("datatype_sym_break", "5"),
    6.10     ("kodkod_sym_break", "15"),
    6.11 @@ -91,7 +90,6 @@
    6.12     ("dont_destroy_constrs", "destroy_constrs"),
    6.13     ("dont_specialize", "specialize"),
    6.14     ("dont_star_linear_preds", "star_linear_preds"),
    6.15 -   ("full_descrs", "fast_descrs"),
    6.16     ("no_peephole_optim", "peephole_optim"),
    6.17     ("no_debug", "debug"),
    6.18     ("quiet", "verbose"),
    6.19 @@ -251,7 +249,6 @@
    6.20      val destroy_constrs = lookup_bool "destroy_constrs"
    6.21      val specialize = lookup_bool "specialize"
    6.22      val star_linear_preds = lookup_bool "star_linear_preds"
    6.23 -    val fast_descrs = lookup_bool "fast_descrs"
    6.24      val peephole_optim = lookup_bool "peephole_optim"
    6.25      val datatype_sym_break = lookup_int "datatype_sym_break"
    6.26      val kodkod_sym_break = lookup_int "kodkod_sym_break"
    6.27 @@ -282,8 +279,8 @@
    6.28       user_axioms = user_axioms, assms = assms, whacks = whacks,
    6.29       merge_type_vars = merge_type_vars, binary_ints = binary_ints,
    6.30       destroy_constrs = destroy_constrs, specialize = specialize,
    6.31 -     star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
    6.32 -     peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
    6.33 +     star_linear_preds = star_linear_preds, peephole_optim = peephole_optim,
    6.34 +     datatype_sym_break = datatype_sym_break,
    6.35       kodkod_sym_break = kodkod_sym_break, timeout = timeout,
    6.36       tac_timeout = tac_timeout, max_threads = max_threads,
    6.37       show_datatypes = show_datatypes, show_consts = show_consts,
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 14 12:52:50 2010 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 14 13:24:18 2010 +0200
     7.3 @@ -872,9 +872,9 @@
     7.4  fun reconstruct_hol_model {show_datatypes, show_consts}
     7.5          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
     7.6                        debug, whacks, binary_ints, destroy_constrs, specialize,
     7.7 -                      star_linear_preds, fast_descrs, tac_timeout, evals,
     7.8 -                      case_names, def_table, nondef_table, user_nondefs,
     7.9 -                      simp_table, psimp_table, choice_spec_table, intro_table,
    7.10 +                      star_linear_preds, tac_timeout, evals, case_names,
    7.11 +                      def_table, nondef_table, user_nondefs, simp_table,
    7.12 +                      psimp_table, choice_spec_table, intro_table,
    7.13                        ground_thm_table, ersatz_table, skolems, special_funs,
    7.14                        unrolled_preds, wf_cache, constr_cache},
    7.15           binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    7.16 @@ -889,15 +889,15 @@
    7.17         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    7.18         whacks = whacks, binary_ints = binary_ints,
    7.19         destroy_constrs = destroy_constrs, specialize = specialize,
    7.20 -       star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
    7.21 -       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
    7.22 -       def_table = def_table, nondef_table = nondef_table,
    7.23 -       user_nondefs = user_nondefs, simp_table = simp_table,
    7.24 -       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    7.25 -       intro_table = intro_table, ground_thm_table = ground_thm_table,
    7.26 -       ersatz_table = ersatz_table, skolems = skolems,
    7.27 -       special_funs = special_funs, unrolled_preds = unrolled_preds,
    7.28 -       wf_cache = wf_cache, constr_cache = constr_cache}
    7.29 +       star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
    7.30 +       evals = evals, case_names = case_names, def_table = def_table,
    7.31 +       nondef_table = nondef_table, user_nondefs = user_nondefs,
    7.32 +       simp_table = simp_table, psimp_table = psimp_table,
    7.33 +       choice_spec_table = choice_spec_table, intro_table = intro_table,
    7.34 +       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    7.35 +       skolems = skolems, special_funs = special_funs,
    7.36 +       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
    7.37 +       constr_cache = constr_cache}
    7.38      val scope =
    7.39        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    7.40         bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 14 12:52:50 2010 +0200
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 14 13:24:18 2010 +0200
     8.3 @@ -549,13 +549,12 @@
     8.4     consts = consts}
     8.5    handle List.Empty => initial_gamma (* FIXME: needed? *)
     8.6  
     8.7 -fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, ...},
     8.8 -                             alpha_T, max_fresh, ...}) =
     8.9 +fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
    8.10 +                             max_fresh, ...}) =
    8.11    let
    8.12      fun is_enough_eta_expanded t =
    8.13        case strip_comb t of
    8.14 -        (Const x, ts) =>
    8.15 -        the_default 0 (arity_of_built_in_const thy stds fast_descrs x)
    8.16 +        (Const x, ts) => the_default 0 (arity_of_built_in_const thy stds x)
    8.17          <= length ts
    8.18        | _ => true
    8.19      val mtype_for = fresh_mtype_for_type mdata false
    8.20 @@ -725,7 +724,7 @@
    8.21                    (mtype_for_sel mdata x, accum)
    8.22                  else if is_constr ctxt stds x then
    8.23                    (mtype_for_constr mdata x, accum)
    8.24 -                else if is_built_in_const thy stds fast_descrs x then
    8.25 +                else if is_built_in_const thy stds x then
    8.26                    (fresh_mtype_for_type mdata true T, accum)
    8.27                  else
    8.28                    let val M = mtype_for T in
    8.29 @@ -908,9 +907,9 @@
    8.30  val bounteous_consts = [@{const_name bisim}]
    8.31  
    8.32  fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
    8.33 -  | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
    8.34 +  | is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
    8.35      Term.add_consts t []
    8.36 -    |> filter_out (is_built_in_const thy stds fast_descrs)
    8.37 +    |> filter_out (is_built_in_const thy stds)
    8.38      |> (forall (member (op =) harmless_consts o original_name o fst) orf
    8.39          exists (member (op =) bounteous_consts o fst))
    8.40  
    8.41 @@ -1022,8 +1021,7 @@
    8.42  fun fin_fun_constr T1 T2 =
    8.43    (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
    8.44  
    8.45 -fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache,
    8.46 -                                ...})
    8.47 +fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...})
    8.48                    binarize finitizes alpha_T tsp =
    8.49    case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
    8.50      SOME (lits, msp, constr_mtypes) =>
    8.51 @@ -1074,7 +1072,7 @@
    8.52                        | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
    8.53                                           \term_from_mterm", [T, T'], [])
    8.54                    in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
    8.55 -                else if is_built_in_const thy stds fast_descrs x then
    8.56 +                else if is_built_in_const thy stds x then
    8.57                    coerce_term hol_ctxt new_Ts T' T t
    8.58                  else if is_constr ctxt stds x then
    8.59                    Const (finitize_constr x)
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Sep 14 12:52:50 2010 +0200
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Sep 14 13:24:18 2010 +0200
     9.3 @@ -430,7 +430,7 @@
     9.4      maps factorize [mk_fst z, mk_snd z]
     9.5    | factorize z = [z]
     9.6  
     9.7 -fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq =
     9.8 +fun nut_from_term (hol_ctxt as {thy, ctxt, stds, ...}) eq =
     9.9    let
    9.10      fun aux eq ss Ts t =
    9.11        let
    9.12 @@ -470,12 +470,6 @@
    9.13              val t1 = list_comb (t0, ts')
    9.14              val T1 = fastype_of1 (Ts, t1)
    9.15            in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
    9.16 -        fun do_description_operator oper undef_s (x as (_, T)) t1 =
    9.17 -          if fast_descrs then
    9.18 -            Op2 (oper, range_type T, Any, sub t1,
    9.19 -                 sub (Const (undef_s, range_type T)))
    9.20 -          else
    9.21 -            do_apply (Const x) [t1]
    9.22          fun do_construct (x as (_, T)) ts =
    9.23            case num_binder_types T - length ts of
    9.24              0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
    9.25 @@ -511,10 +505,6 @@
    9.26            do_quantifier Exist s T t1
    9.27          | (t0 as Const (@{const_name Ex}, _), [t1]) =>
    9.28            sub' (t0 $ eta_expand Ts t1 1)
    9.29 -        | (Const (x as (@{const_name The}, _)), [t1]) =>
    9.30 -          do_description_operator The @{const_name undefined_fast_The} x t1
    9.31 -        | (Const (x as (@{const_name Eps}, _)), [t1]) =>
    9.32 -          do_description_operator Eps @{const_name undefined_fast_Eps} x t1
    9.33          | (Const (@{const_name HOL.eq}, T), [t1]) =>
    9.34            Op1 (SingletonSet, range_type T, Any, sub t1)
    9.35          | (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2
    9.36 @@ -549,7 +539,7 @@
    9.37          | (Const (@{const_name image}, T), [t1, t2]) =>
    9.38            Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
    9.39          | (Const (x as (s as @{const_name Suc}, T)), []) =>
    9.40 -          if is_built_in_const thy stds false x then Cst (Suc, T, Any)
    9.41 +          if is_built_in_const thy stds x then Cst (Suc, T, Any)
    9.42            else if is_constr ctxt stds x then do_construct x []
    9.43            else ConstName (s, T, Any)
    9.44          | (Const (@{const_name finite}, T), [t1]) =>
    9.45 @@ -560,27 +550,27 @@
    9.46             | _ => Op1 (Finite, bool_T, Any, sub t1))
    9.47          | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
    9.48          | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
    9.49 -          if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
    9.50 +          if is_built_in_const thy stds x then Cst (Num 0, T, Any)
    9.51            else if is_constr ctxt stds x then do_construct x []
    9.52            else ConstName (s, T, Any)
    9.53          | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
    9.54 -          if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
    9.55 +          if is_built_in_const thy stds x then Cst (Num 1, T, Any)
    9.56            else ConstName (s, T, Any)
    9.57          | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
    9.58 -          if is_built_in_const thy stds false x then Cst (Add, T, Any)
    9.59 +          if is_built_in_const thy stds x then Cst (Add, T, Any)
    9.60            else ConstName (s, T, Any)
    9.61          | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
    9.62 -          if is_built_in_const thy stds false x then Cst (Subtract, T, Any)
    9.63 +          if is_built_in_const thy stds x then Cst (Subtract, T, Any)
    9.64            else ConstName (s, T, Any)
    9.65          | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
    9.66 -          if is_built_in_const thy stds false x then Cst (Multiply, T, Any)
    9.67 +          if is_built_in_const thy stds x then Cst (Multiply, T, Any)
    9.68            else ConstName (s, T, Any)
    9.69          | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
    9.70 -          if is_built_in_const thy stds false x then Cst (Divide, T, Any)
    9.71 +          if is_built_in_const thy stds x then Cst (Divide, T, Any)
    9.72            else ConstName (s, T, Any)
    9.73          | (t0 as Const (x as (@{const_name ord_class.less}, _)),
    9.74             ts as [t1, t2]) =>
    9.75 -          if is_built_in_const thy stds false x then
    9.76 +          if is_built_in_const thy stds x then
    9.77              Op2 (Less, bool_T, Any, sub t1, sub t2)
    9.78            else
    9.79              do_apply t0 ts
    9.80 @@ -592,14 +582,14 @@
    9.81          (* FIXME: find out if this case is necessary *)
    9.82          | (t0 as Const (x as (@{const_name ord_class.less_eq}, _)),
    9.83             ts as [t1, t2]) =>
    9.84 -          if is_built_in_const thy stds false x then
    9.85 +          if is_built_in_const thy stds x then
    9.86              Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
    9.87            else
    9.88              do_apply t0 ts
    9.89          | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
    9.90          | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
    9.91          | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
    9.92 -          if is_built_in_const thy stds false x then
    9.93 +          if is_built_in_const thy stds x then
    9.94              let val num_T = domain_type T in
    9.95                Op2 (Apply, num_T --> num_T, Any,
    9.96                     Cst (Subtract, num_T --> num_T --> num_T, Any),
    9.97 @@ -613,8 +603,6 @@
    9.98          | (Const (@{const_name safe_The},
    9.99                    Type (@{type_name fun}, [_, T2])), [t1]) =>
   9.100            Op1 (SafeThe, T2, Any, sub t1)
   9.101 -        | (Const (x as (@{const_name safe_Eps}, _)), [t1]) =>
   9.102 -          do_description_operator Eps @{const_name undefined_fast_Eps} x t1
   9.103          | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
   9.104          | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
   9.105          | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
   9.106 @@ -628,7 +616,7 @@
   9.107            else if String.isPrefix numeral_prefix s then
   9.108              Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
   9.109            else
   9.110 -            (case arity_of_built_in_const thy stds fast_descrs x of
   9.111 +            (case arity_of_built_in_const thy stds x of
   9.112                 SOME n =>
   9.113                 (case n - length ts of
   9.114                    0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Sep 14 12:52:50 2010 +0200
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Sep 14 13:24:18 2010 +0200
    10.3 @@ -76,7 +76,7 @@
    10.4          let val table = aux t2 [] table in aux t1 (t2 :: args) table end
    10.5        | aux (Abs (_, _, t')) _ table = aux t' [] table
    10.6        | aux (t as Const (x as (s, _))) args table =
    10.7 -        if is_built_in_const thy [(NONE, true)] true x orelse
    10.8 +        if is_built_in_const thy [(NONE, true)] x orelse
    10.9             is_constr_like ctxt x orelse
   10.10             is_sel s orelse s = @{const_name Sigma} then
   10.11            table
   10.12 @@ -127,8 +127,7 @@
   10.13  
   10.14  (** Boxing **)
   10.15  
   10.16 -fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...})
   10.17 -                             def orig_t =
   10.18 +fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, ...}) def orig_t =
   10.19    let
   10.20      fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
   10.21          Type (@{type_name fun}, map box_relational_operator_type Ts)
   10.22 @@ -231,7 +230,7 @@
   10.23                        let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
   10.24                          T' --> T'
   10.25                        end
   10.26 -                    else if is_built_in_const thy stds fast_descrs x orelse
   10.27 +                    else if is_built_in_const thy stds x orelse
   10.28                              s = @{const_name Sigma} then
   10.29                        T
   10.30                      else if is_constr_like ctxt x then
   10.31 @@ -732,8 +731,8 @@
   10.32    forall (op aconv) (ts1 ~~ ts2)
   10.33  
   10.34  fun specialize_consts_in_term
   10.35 -        (hol_ctxt as {ctxt, thy, stds, specialize, fast_descrs, def_table,
   10.36 -                      simp_table, special_funs, ...}) def depth t =
   10.37 +        (hol_ctxt as {ctxt, thy, stds, specialize, def_table, simp_table,
   10.38 +                      special_funs, ...}) def depth t =
   10.39    if not specialize orelse depth > special_max_depth then
   10.40      t
   10.41    else
   10.42 @@ -743,7 +742,7 @@
   10.43        fun aux args Ts (Const (x as (s, T))) =
   10.44            ((if not (member (op =) blacklist x) andalso not (null args) andalso
   10.45                 not (String.isPrefix special_prefix s) andalso
   10.46 -               not (is_built_in_const thy stds fast_descrs x) andalso
   10.47 +               not (is_built_in_const thy stds x) andalso
   10.48                 (is_equational_fun_but_no_plain_def hol_ctxt x orelse
   10.49                  (is_some (def_of_const thy def_table x) andalso
   10.50                   not (is_of_class_const thy x) andalso
   10.51 @@ -894,8 +893,8 @@
   10.52  
   10.53  fun axioms_for_term
   10.54          (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
   10.55 -                      fast_descrs, evals, def_table, nondef_table,
   10.56 -                      choice_spec_table, user_nondefs, ...}) assm_ts neg_t =
   10.57 +                      evals, def_table, nondef_table, choice_spec_table,
   10.58 +                      user_nondefs, ...}) assm_ts neg_t =
   10.59    let
   10.60      val (def_assm_ts, nondef_assm_ts) =
   10.61        List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
   10.62 @@ -926,8 +925,7 @@
   10.63        case t of
   10.64          t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
   10.65        | Const (x as (s, T)) =>
   10.66 -        (if member (op aconv) seen t orelse
   10.67 -            is_built_in_const thy stds fast_descrs x then
   10.68 +        (if member (op aconv) seen t orelse is_built_in_const thy stds x then
   10.69             accum
   10.70           else
   10.71             let val accum = (t :: seen, axs) in