internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
authorblanchet
Tue Oct 27 14:40:24 2009 +0100 (2009-10-27)
changeset 33232f93390060bbe
parent 33231 1711610c5b7d
child 33233 f9ff11344ec4
child 33238 aac547760e16
child 33260 f8d43d5215c2
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi
doc-src/Nitpick/nitpick.tex
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Nitpick_Examples/Tests_Nits.thy
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/kodkod_sat.ML
src/HOL/Tools/Nitpick/minipick.ML
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_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_peephole.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Oct 27 12:16:26 2009 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Oct 27 14:40:24 2009 +0100
     1.3 @@ -2381,7 +2381,7 @@
     1.4  (``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
     1.5  \textit{params} type is a large record that lets you set Nitpick's options. The
     1.6  current default options can be retrieved by calling the following function
     1.7 -defined in the \textit{NitpickIsar} structure:
     1.8 +defined in the \textit{Nitpick\_Isar} structure:
     1.9  
    1.10  \prew
    1.11  $\textbf{val}\,~\textit{default\_params} :\,
    1.12 @@ -2392,7 +2392,7 @@
    1.13  put into a \textit{params} record. Here is an example:
    1.14  
    1.15  \prew
    1.16 -$\textbf{val}\,~\textit{params} = \textit{NitpickIsar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
    1.17 +$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
    1.18  $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
    1.19  & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
    1.20  & \textit{subgoal}\end{aligned}$
     2.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Oct 27 12:16:26 2009 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Oct 27 14:40:24 2009 +0100
     2.3 @@ -14,8 +14,8 @@
     2.4  ML {*
     2.5  exception FAIL
     2.6  
     2.7 -val defs = NitpickHOL.all_axioms_of @{theory} |> #1
     2.8 -val def_table = NitpickHOL.const_def_table @{context} defs
     2.9 +val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
    2.10 +val def_table = Nitpick_HOL.const_def_table @{context} defs
    2.11  val ext_ctxt =
    2.12    {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
    2.13     user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false,
     3.1 --- a/src/HOL/Nitpick_Examples/Tests_Nits.thy	Tue Oct 27 12:16:26 2009 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy	Tue Oct 27 14:40:24 2009 +0100
     3.3 @@ -11,6 +11,6 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -ML {* NitpickTests.run_all_tests () *}
     3.8 +ML {* Nitpick_Tests.run_all_tests () *}
     3.9  
    3.10  end
     4.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Oct 27 12:16:26 2009 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Tue Oct 27 14:40:24 2009 +0100
     4.3 @@ -1044,7 +1044,10 @@
     4.4                val code =
     4.5                  system ("env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
     4.6                          \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
     4.7 -                        \$JAVA_LIBRARY_PATH\" \"$ISABELLE_TOOL\" java \
     4.8 +                        \$JAVA_LIBRARY_PATH\" \
     4.9 +                        \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
    4.10 +                        \$LD_LIBRARY_PATH\" \
    4.11 +                        \\"$ISABELLE_TOOL\" java \
    4.12                          \de.tum.in.isabelle.Kodkodi.Kodkodi" ^
    4.13                          (if ms >= 0 then " -max-msecs " ^ Int.toString ms
    4.14                           else "") ^
     5.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Tue Oct 27 12:16:26 2009 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Tue Oct 27 14:40:24 2009 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4    val sat_solver_spec : string -> string * string list
     5.5  end;
     5.6  
     5.7 -structure KodkodSAT : KODKOD_SAT =
     5.8 +structure Kodkod_SAT : KODKOD_SAT =
     5.9  struct
    5.10  
    5.11  datatype sink = ToStdout | ToFile
     6.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Tue Oct 27 12:16:26 2009 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Tue Oct 27 14:40:24 2009 +0100
     6.3 @@ -14,10 +14,10 @@
     6.4  struct
     6.5  
     6.6  open Kodkod
     6.7 -open NitpickUtil
     6.8 -open NitpickHOL
     6.9 -open NitpickPeephole
    6.10 -open NitpickKodkod
    6.11 +open Nitpick_Util
    6.12 +open Nitpick_HOL
    6.13 +open Nitpick_Peephole
    6.14 +open Nitpick_Kodkod
    6.15  
    6.16  (* theory -> typ -> unit *)
    6.17  fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 12:16:26 2009 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 14:40:24 2009 +0100
     7.3 @@ -62,15 +62,15 @@
     7.4  structure Nitpick : NITPICK =
     7.5  struct
     7.6  
     7.7 -open NitpickUtil
     7.8 -open NitpickHOL
     7.9 -open NitpickMono
    7.10 -open NitpickScope
    7.11 -open NitpickPeephole
    7.12 -open NitpickRep
    7.13 -open NitpickNut
    7.14 -open NitpickKodkod
    7.15 -open NitpickModel
    7.16 +open Nitpick_Util
    7.17 +open Nitpick_HOL
    7.18 +open Nitpick_Mono
    7.19 +open Nitpick_Scope
    7.20 +open Nitpick_Peephole
    7.21 +open Nitpick_Rep
    7.22 +open Nitpick_Nut
    7.23 +open Nitpick_Kodkod
    7.24 +open Nitpick_Model
    7.25  
    7.26  type params = {
    7.27    cards_assigns: (typ option * int list) list,
    7.28 @@ -355,21 +355,21 @@
    7.29      val effective_sat_solver =
    7.30        if sat_solver <> "smart" then
    7.31          if need_incremental andalso
    7.32 -           not (sat_solver mem KodkodSAT.configured_sat_solvers true) then
    7.33 +           not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then
    7.34            (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
    7.35                         \be used instead of " ^ quote sat_solver ^ "."));
    7.36             "SAT4J")
    7.37          else
    7.38            sat_solver
    7.39        else
    7.40 -        KodkodSAT.smart_sat_solver_name need_incremental
    7.41 +        Kodkod_SAT.smart_sat_solver_name need_incremental
    7.42      val _ =
    7.43        if sat_solver = "smart" then
    7.44          print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^
    7.45                            ". The following" ^
    7.46                            (if need_incremental then " incremental " else " ") ^
    7.47                            "solvers are configured: " ^
    7.48 -                          commas (map quote (KodkodSAT.configured_sat_solvers
    7.49 +                          commas (map quote (Kodkod_SAT.configured_sat_solvers
    7.50                                                         need_incremental)) ^ ".")
    7.51        else
    7.52          ()
    7.53 @@ -439,7 +439,7 @@
    7.54          val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
    7.55          val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
    7.56                        PrintMode.setmp [] multiline_string_for_scope scope
    7.57 -        val kodkod_sat_solver = KodkodSAT.sat_solver_spec effective_sat_solver
    7.58 +        val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver
    7.59                                  |> snd
    7.60          val delay = if liberal then
    7.61                        Option.map (fn time => Time.- (time, Time.now ()))
    7.62 @@ -483,7 +483,7 @@
    7.63                 defs = nondef_fs @ def_fs @ declarative_axioms})
    7.64        end
    7.65        handle LIMIT (loc, msg) =>
    7.66 -             if loc = "NitpickKodkod.check_arity"
    7.67 +             if loc = "Nitpick_Kodkod.check_arity"
    7.68                  andalso not (Typtab.is_empty ofs) then
    7.69                 problem_for_scope liberal
    7.70                     {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 12:16:26 2009 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 14:40:24 2009 +0100
     8.3 @@ -139,10 +139,10 @@
     8.4      extended_context -> term -> ((term list * term list) * (bool * bool)) * term
     8.5  end;
     8.6  
     8.7 -structure NitpickHOL : NITPICK_HOL =
     8.8 +structure Nitpick_HOL : NITPICK_HOL =
     8.9  struct
    8.10  
    8.11 -open NitpickUtil
    8.12 +open Nitpick_Util
    8.13  
    8.14  type const_table = term list Symtab.table
    8.15  type special_fun = (styp * int list * term list) * styp
    8.16 @@ -263,7 +263,7 @@
    8.17  val after_name_sep = snd o strip_first_name_sep
    8.18  
    8.19  (* When you add constants to these lists, make sure to handle them in
    8.20 -   "NitpickNut.nut_from_term", and perhaps in "NitpickMono.consider_term" as
    8.21 +   "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
    8.22     well. *)
    8.23  val built_in_consts =
    8.24    [(@{const_name all}, 1),
    8.25 @@ -405,7 +405,7 @@
    8.26  (* typ -> styp *)
    8.27  fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
    8.28    | const_for_iterator_type T =
    8.29 -    raise TYPE ("NitpickHOL.const_for_iterator_type", [T], [])
    8.30 +    raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
    8.31  
    8.32  (* int -> typ -> typ * typ *)
    8.33  fun strip_n_binders 0 T = ([], T)
    8.34 @@ -413,7 +413,7 @@
    8.35      strip_n_binders (n - 1) T2 |>> cons T1
    8.36    | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
    8.37      strip_n_binders n (Type ("fun", Ts))
    8.38 -  | strip_n_binders _ T = raise TYPE ("NitpickHOL.strip_n_binders", [T], [])
    8.39 +  | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
    8.40  (* typ -> typ *)
    8.41  val nth_range_type = snd oo strip_n_binders
    8.42  
    8.43 @@ -432,7 +432,7 @@
    8.44  fun mk_flat_tuple _ [t] = t
    8.45    | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
    8.46      HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
    8.47 -  | mk_flat_tuple T ts = raise TYPE ("NitpickHOL.mk_flat_tuple", [T], ts)
    8.48 +  | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
    8.49  (* int -> term -> term list *)
    8.50  fun dest_n_tuple 1 t = [t]
    8.51    | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
    8.52 @@ -441,7 +441,8 @@
    8.53  fun dest_n_tuple_type 1 T = [T]
    8.54    | dest_n_tuple_type n (Type (_, [T1, T2])) =
    8.55      T1 :: dest_n_tuple_type (n - 1) T2
    8.56 -  | dest_n_tuple_type _ T = raise TYPE ("NitpickHOL.dest_n_tuple_type", [T], [])
    8.57 +  | dest_n_tuple_type _ T =
    8.58 +    raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
    8.59  
    8.60  (* (typ * typ) list -> typ -> typ *)
    8.61  fun typ_subst [] T = T
    8.62 @@ -460,7 +461,7 @@
    8.63                     (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
    8.64                (Logic.varifyT T2)
    8.65    handle Type.TYPE_MATCH =>
    8.66 -         raise TYPE ("NitpickHOL.instantiate_type", [T1, T1'], [])
    8.67 +         raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
    8.68  
    8.69  (* theory -> typ -> typ -> styp *)
    8.70  fun repair_constr_type thy body_T' T =
    8.71 @@ -483,7 +484,7 @@
    8.72      val (co_s, co_Ts) = dest_Type co_T
    8.73      val _ =
    8.74        if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()
    8.75 -      else raise TYPE ("NitpickHOL.register_codatatype", [co_T], [])
    8.76 +      else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
    8.77      val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
    8.78                                     codatatypes
    8.79    in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
    8.80 @@ -586,8 +587,8 @@
    8.81  fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
    8.82      (case typedef_info thy s' of
    8.83         SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
    8.84 -     | NONE => raise TERM ("NitpickHOL.mate_of_rep_fun", [Const x]))
    8.85 -  | mate_of_rep_fun _ x = raise TERM ("NitpickHOL.mate_of_rep_fun", [Const x])
    8.86 +     | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
    8.87 +  | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
    8.88  
    8.89  (* theory -> styp -> bool *)
    8.90  fun is_coconstr thy (s, T) =
    8.91 @@ -874,7 +875,7 @@
    8.92      case AList.lookup (op =) asgns T of
    8.93        SOME k => k
    8.94      | NONE => if T = @{typ bisim_iterator} then 0
    8.95 -              else raise TYPE ("NitpickHOL.card_of_type", [T], [])
    8.96 +              else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
    8.97  (* int -> (typ * int) list -> typ -> int *)
    8.98  fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) =
    8.99      let
   8.100 @@ -894,7 +895,7 @@
   8.101                      card_of_type asgns T
   8.102                    else
   8.103                      card_of_type asgns T
   8.104 -                    handle TYPE ("NitpickHOL.card_of_type", _, _) =>
   8.105 +                    handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   8.106                             default_card)
   8.107  (* theory -> int -> (typ * int) list -> typ -> int *)
   8.108  fun bounded_precise_card_of_type thy max default_card asgns T =
   8.109 @@ -1110,13 +1111,13 @@
   8.110      (* term -> term *)
   8.111      fun aux (v as Var _) t = lambda v t
   8.112        | aux (c as Const (@{const_name TYPE}, T)) t = lambda c t
   8.113 -      | aux _ _ = raise TERM ("NitpickHOL.normalized_rhs_of", [t])
   8.114 +      | aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
   8.115      val (lhs, rhs) =
   8.116        case t of
   8.117          Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
   8.118        | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
   8.119          (t1, t2)
   8.120 -      | _ => raise TERM ("NitpickHOL.normalized_rhs_of", [t])
   8.121 +      | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
   8.122      val args = strip_comb lhs |> snd
   8.123    in fold_rev aux args rhs end
   8.124  
   8.125 @@ -1170,7 +1171,7 @@
   8.126    case term_under_def t of
   8.127      Const (s, _) => (s, t)
   8.128    | Free _ => raise NOT_SUPPORTED "local definitions"
   8.129 -  | t' => raise TERM ("NitpickHOL.pair_for_prop", [t, t'])
   8.130 +  | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
   8.131  
   8.132  (* (Proof.context -> term list) -> Proof.context -> const_table *)
   8.133  fun table_for get ctxt =
   8.134 @@ -1308,7 +1309,7 @@
   8.135      |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   8.136    end
   8.137  
   8.138 -val redefined_in_NitpickDefs_thy =
   8.139 +val redefined_in_Nitpick_thy =
   8.140    [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
   8.141     @{const_name list_size}]
   8.142  
   8.143 @@ -1325,7 +1326,8 @@
   8.144                   select_nth_constr_arg thy constr_x t j res_T
   8.145                   |> optimized_record_get thy s rec_T' res_T
   8.146                 end
   8.147 -             | _ => raise TYPE ("NitpickHOL.optimized_record_get", [rec_T], []))
   8.148 +             | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
   8.149 +                                []))
   8.150      | j => select_nth_constr_arg thy constr_x t j res_T
   8.151    end
   8.152  (* theory -> string -> typ -> term -> term -> term *)
   8.153 @@ -1380,7 +1382,7 @@
   8.154    (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
   8.155     orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
   8.156    andf (not o has_trivial_definition thy def_table)
   8.157 -  andf (not o member (op =) redefined_in_NitpickDefs_thy o fst)
   8.158 +  andf (not o member (op =) redefined_in_Nitpick_thy o fst)
   8.159  
   8.160  (* term * term -> term *)
   8.161  fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
   8.162 @@ -1532,7 +1534,7 @@
   8.163                else case def_of_const thy def_table x of
   8.164                  SOME def =>
   8.165                  if depth > unfold_max_depth then
   8.166 -                  raise LIMIT ("NitpickHOL.unfold_defs_in_term",
   8.167 +                  raise LIMIT ("Nitpick_HOL.unfold_defs_in_term",
   8.168                                 "too many nested definitions (" ^
   8.169                                 string_of_int depth ^ ") while expanding " ^
   8.170                                 quote s)
   8.171 @@ -1640,7 +1642,8 @@
   8.172          ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
   8.173           : extended_context) (x as (_, T)) =
   8.174    case def_props_for_const thy fast_descrs intro_table x of
   8.175 -    [] => raise TERM ("NitpickHOL.is_is_well_founded_inductive_pred", [Const x])
   8.176 +    [] => raise TERM ("Nitpick_HOL.is_is_well_founded_inductive_pred",
   8.177 +                      [Const x])
   8.178    | intro_ts =>
   8.179      (case map (triple_for_intro_rule thy x) intro_ts
   8.180            |> filter_out (null o #2) of
   8.181 @@ -1772,7 +1775,7 @@
   8.182                                |> ap_split tuple_T bool_T))
   8.183          end
   8.184        | aux t =
   8.185 -        raise TERM ("NitpickHOL.linear_pred_base_and_step_rhss.aux", [t])
   8.186 +        raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
   8.187    in aux end
   8.188  
   8.189  (* extended_context -> styp -> term -> term *)
   8.190 @@ -1834,8 +1837,8 @@
   8.191          val rhs = case fp_app of
   8.192                      Const _ $ t =>
   8.193                      betapply (t, list_comb (Const x', next :: outer_bounds))
   8.194 -                  | _ => raise TERM ("NitpickHOL.unrolled_inductive_pred_const",
   8.195 -                                     [fp_app])
   8.196 +                  | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
   8.197 +                                     \const", [fp_app])
   8.198          val (inner, naked_rhs) = strip_abs rhs
   8.199          val all = outer @ inner
   8.200          val bounds = map Bound (length all - 1 downto 0)
   8.201 @@ -1854,7 +1857,7 @@
   8.202      val outer_bounds = map Bound (length outer - 1 downto 0)
   8.203      val rhs = case fp_app of
   8.204                  Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
   8.205 -              | _ => raise TERM ("NitpickHOL.raw_inductive_pred_axiom",
   8.206 +              | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
   8.207                                   [fp_app])
   8.208      val (inner, naked_rhs) = strip_abs rhs
   8.209      val all = outer @ inner
   8.210 @@ -1876,7 +1879,7 @@
   8.211  (* extended_context -> styp -> term list *)
   8.212  fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
   8.213                                              psimp_table, ...}) (x as (s, _)) =
   8.214 -  if s mem redefined_in_NitpickDefs_thy then
   8.215 +  if s mem redefined_in_Nitpick_thy then
   8.216      []
   8.217    else case def_props_for_const thy fast_descrs (!simp_table) x of
   8.218      [] => (case def_props_for_const thy fast_descrs psimp_table x of
   8.219 @@ -2329,7 +2332,7 @@
   8.220                                  ts
   8.221                     (* (term * int list) list -> term *)
   8.222                     fun mk_connection [] =
   8.223 -                       raise ARG ("NitpickHOL.push_quantifiers_inward.aux.\
   8.224 +                       raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
   8.225                                    \mk_connection", "")
   8.226                       | mk_connection ts_cum_bounds =
   8.227                         ts_cum_bounds |> map fst
   8.228 @@ -2720,7 +2723,7 @@
   8.229               |> new_s <> "fun"
   8.230                  ? construct_value thy (@{const_name FunBox},
   8.231                                         Type ("fun", new_Ts) --> new_T) o single
   8.232 -           | t' => raise TERM ("NitpickHOL.box_fun_and_pair_in_term.\
   8.233 +           | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
   8.234                                 \coerce_term", [t']))
   8.235          | (Type (new_s, new_Ts as [new_T1, new_T2]),
   8.236             Type (old_s, old_Ts as [old_T1, old_T2])) =>
   8.237 @@ -2740,7 +2743,7 @@
   8.238                     else @{const_name PairBox}, new_Ts ---> new_T)
   8.239                    [coerce_term Ts new_T1 old_T1 t1,
   8.240                     coerce_term Ts new_T2 old_T2 t2]
   8.241 -            | t' => raise TERM ("NitpickHOL.box_fun_and_pair_in_term.\
   8.242 +            | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
   8.243                                  \coerce_term", [t'])
   8.244            else
   8.245              raise TYPE ("coerce_term", [new_T, old_T], [t])
   8.246 @@ -2753,7 +2756,7 @@
   8.247          (case T' of
   8.248             Type (_, [T1, T2]) =>
   8.249             fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
   8.250 -         | _ => raise TYPE ("NitpickHOL.box_fun_and_pair_in_term.\
   8.251 +         | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
   8.252                              \add_boxed_types_for_var", [T'], []))
   8.253        | _ => exists_subterm (equal (Var z)) t' ? insert (op =) T
   8.254      (* typ list -> typ list -> term -> indexname * typ -> typ *)
   8.255 @@ -3008,7 +3011,7 @@
   8.256           else
   8.257             let val accum as (xs, _) = (x :: xs, axs) in
   8.258               if depth > axioms_max_depth then
   8.259 -               raise LIMIT ("NitpickHOL.axioms_for_term.add_axioms_for_term",
   8.260 +               raise LIMIT ("Nitpick_HOL.axioms_for_term.add_axioms_for_term",
   8.261                              "too many nested axioms (" ^ string_of_int depth ^
   8.262                              ")")
   8.263               else if Refute.is_const_of_class thy x then
   8.264 @@ -3081,7 +3084,7 @@
   8.265                           [] => t
   8.266                         | [(x, S)] =>
   8.267                           Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
   8.268 -                       | _ => raise TERM ("NitpickHOL.axioms_for_term.\
   8.269 +                       | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
   8.270                                            \add_axioms_for_sort", [t]))
   8.271                class_axioms
   8.272        in fold (add_nondef_axiom depth) monomorphic_class_axioms end
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 12:16:26 2009 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 14:40:24 2009 +0100
     9.3 @@ -13,13 +13,13 @@
     9.4    val default_params : theory -> (string * string) list -> params
     9.5  end
     9.6  
     9.7 -structure NitpickIsar : NITPICK_ISAR =
     9.8 +structure Nitpick_Isar : NITPICK_ISAR =
     9.9  struct
    9.10  
    9.11 -open NitpickUtil
    9.12 -open NitpickHOL
    9.13 -open NitpickRep
    9.14 -open NitpickNut
    9.15 +open Nitpick_Util
    9.16 +open Nitpick_HOL
    9.17 +open Nitpick_Rep
    9.18 +open Nitpick_Nut
    9.19  open Nitpick
    9.20  
    9.21  type raw_param = string * string list
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Oct 27 12:16:26 2009 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Oct 27 14:40:24 2009 +0100
    10.3 @@ -7,10 +7,10 @@
    10.4  
    10.5  signature NITPICK_KODKOD =
    10.6  sig
    10.7 -  type extended_context = NitpickHOL.extended_context
    10.8 -  type dtype_spec = NitpickScope.dtype_spec
    10.9 -  type kodkod_constrs = NitpickPeephole.kodkod_constrs
   10.10 -  type nut = NitpickNut.nut
   10.11 +  type extended_context = Nitpick_HOL.extended_context
   10.12 +  type dtype_spec = Nitpick_Scope.dtype_spec
   10.13 +  type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
   10.14 +  type nut = Nitpick_Nut.nut
   10.15    type nfa_transition = Kodkod.rel_expr * typ
   10.16    type nfa_entry = typ * nfa_transition list
   10.17    type nfa_table = nfa_entry list
   10.18 @@ -37,15 +37,15 @@
   10.19      int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
   10.20  end;
   10.21  
   10.22 -structure NitpickKodkod : NITPICK_KODKOD =
   10.23 +structure Nitpick_Kodkod : NITPICK_KODKOD =
   10.24  struct
   10.25  
   10.26 -open NitpickUtil
   10.27 -open NitpickHOL
   10.28 -open NitpickScope
   10.29 -open NitpickPeephole
   10.30 -open NitpickRep
   10.31 -open NitpickNut
   10.32 +open Nitpick_Util
   10.33 +open Nitpick_HOL
   10.34 +open Nitpick_Scope
   10.35 +open Nitpick_Peephole
   10.36 +open Nitpick_Rep
   10.37 +open Nitpick_Nut
   10.38  
   10.39  type nfa_transition = Kodkod.rel_expr * typ
   10.40  type nfa_entry = typ * nfa_transition list
   10.41 @@ -89,7 +89,7 @@
   10.42  (* int -> int -> unit *)
   10.43  fun check_arity univ_card n =
   10.44    if n > Kodkod.max_arity univ_card then
   10.45 -    raise LIMIT ("NitpickKodkod.check_arity",
   10.46 +    raise LIMIT ("Nitpick_Kodkod.check_arity",
   10.47                   "arity " ^ string_of_int n ^ " too large for universe of \
   10.48                   \cardinality " ^ string_of_int univ_card)
   10.49    else
   10.50 @@ -132,7 +132,7 @@
   10.51  (* int -> unit *)
   10.52  fun check_table_size k =
   10.53    if k > max_table_size then
   10.54 -    raise LIMIT ("NitpickKodkod.check_table_size",
   10.55 +    raise LIMIT ("Nitpick_Kodkod.check_table_size",
   10.56                   "precomputed table too large (" ^ string_of_int k ^ ")")
   10.57    else
   10.58      ()
   10.59 @@ -245,7 +245,7 @@
   10.60       ("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0)
   10.61                                        isa_norm_frac)
   10.62     else
   10.63 -     raise ARG ("NitpickKodkod.tabulate_built_in_rel", "unknown relation"))
   10.64 +     raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
   10.65  
   10.66  (* bool -> int -> int -> int -> int -> int * int -> Kodkod.rel_expr
   10.67     -> Kodkod.bound *)
   10.68 @@ -266,11 +266,11 @@
   10.69       if nick = @{const_name bisim_iterator_max} then
   10.70         case R of
   10.71           Atom (k, j0) => [Kodkod.TupleSet [Kodkod.Tuple [k - 1 + j0]]]
   10.72 -       | _ => raise NUT ("NitpickKodkod.bound_for_plain_rel", [u])
   10.73 +       | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
   10.74       else
   10.75         [Kodkod.TupleSet [], upper_bound_for_rep R])
   10.76    | bound_for_plain_rel _ _ u =
   10.77 -    raise NUT ("NitpickKodkod.bound_for_plain_rel", [u])
   10.78 +    raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
   10.79  
   10.80  (* Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound *)
   10.81  fun bound_for_sel_rel ctxt debug dtypes
   10.82 @@ -293,7 +293,7 @@
   10.83           end)
   10.84      end
   10.85    | bound_for_sel_rel _ _ _ u =
   10.86 -    raise NUT ("NitpickKodkod.bound_for_sel_rel", [u])
   10.87 +    raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
   10.88  
   10.89  (* Kodkod.bound list -> Kodkod.bound list *)
   10.90  fun merge_bounds bs =
   10.91 @@ -320,7 +320,7 @@
   10.92    if is_lone_rep R then
   10.93      all_combinations_for_rep R |> map singleton_from_combination
   10.94    else
   10.95 -    raise REP ("NitpickKodkod.all_singletons_for_rep", [R])
   10.96 +    raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R])
   10.97  
   10.98  (* Kodkod.rel_expr -> Kodkod.rel_expr list *)
   10.99  fun unpack_products (Kodkod.Product (r1, r2)) =
  10.100 @@ -333,7 +333,7 @@
  10.101  val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
  10.102  fun full_rel_for_rep R =
  10.103    case atom_schema_of_rep R of
  10.104 -    [] => raise REP ("NitpickKodkod.full_rel_for_rep", [R])
  10.105 +    [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
  10.106    | schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema)
  10.107  
  10.108  (* int -> int list -> Kodkod.decl list *)
  10.109 @@ -424,7 +424,7 @@
  10.110  fun rel_expr_from_formula kk R f =
  10.111    case unopt_rep R of
  10.112      Atom (2, j0) => atom_from_formula kk j0 f
  10.113 -  | _ => raise REP ("NitpickKodkod.rel_expr_from_formula", [R])
  10.114 +  | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R])
  10.115  
  10.116  (* kodkod_cotrs -> int -> int -> Kodkod.rel_expr -> Kodkod.rel_expr list *)
  10.117  fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity
  10.118 @@ -471,13 +471,13 @@
  10.119        if is_lone_rep old_R andalso is_lone_rep new_R
  10.120           andalso card = card_of_rep new_R then
  10.121          if card >= lone_rep_fallback_max_card then
  10.122 -          raise LIMIT ("NitpickKodkod.lone_rep_fallback",
  10.123 +          raise LIMIT ("Nitpick_Kodkod.lone_rep_fallback",
  10.124                         "too high cardinality (" ^ string_of_int card ^ ")")
  10.125          else
  10.126            kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)
  10.127                           (all_singletons_for_rep new_R)
  10.128        else
  10.129 -        raise REP ("NitpickKodkod.lone_rep_fallback", [old_R, new_R])
  10.130 +        raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
  10.131      end
  10.132  (* kodkod_constrs -> int * int -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  10.133  and atom_from_rel_expr kk (x as (k, j0)) old_R r =
  10.134 @@ -490,7 +490,7 @@
  10.135        atom_from_rel_expr kk x (Vect (dom_card, R2'))
  10.136                           (vect_from_rel_expr kk dom_card R2' old_R r)
  10.137      end
  10.138 -  | Opt _ => raise REP ("NitpickKodkod.atom_from_rel_expr", [old_R])
  10.139 +  | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R])
  10.140    | _ => lone_rep_fallback kk (Atom x) old_R r
  10.141  (* kodkod_constrs -> rep list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  10.142  and struct_from_rel_expr kk Rs old_R r =
  10.143 @@ -515,7 +515,7 @@
  10.144        else
  10.145          lone_rep_fallback kk (Struct Rs) old_R r
  10.146      end
  10.147 -  | _ => raise REP ("NitpickKodkod.struct_from_rel_expr", [old_R])
  10.148 +  | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
  10.149  (* kodkod_constrs -> int -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  10.150  and vect_from_rel_expr kk k R old_R r =
  10.151    case old_R of
  10.152 @@ -530,7 +530,7 @@
  10.153                       rel_expr_from_formula kk R (#kk_subset kk arg_r r))
  10.154                   (all_singletons_for_rep R1))
  10.155      else
  10.156 -      raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R])
  10.157 +      raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
  10.158    | Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r
  10.159    | Func (R1, R2) =>
  10.160      fold1 (#kk_product kk)
  10.161 @@ -538,7 +538,7 @@
  10.162                     rel_expr_from_rel_expr kk R R2
  10.163                                           (kk_n_fold_join kk true R1 R2 arg_r r))
  10.164                 (all_singletons_for_rep R1))
  10.165 -  | _ => raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R])
  10.166 +  | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
  10.167  (* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  10.168  and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r =
  10.169      let
  10.170 @@ -555,12 +555,12 @@
  10.171       | Func (Atom (1, _), Formula Neut) =>
  10.172         (case unopt_rep R2 of
  10.173            Atom (2, j0) => atom_from_formula kk j0 (#kk_some kk r)
  10.174 -        | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
  10.175 +        | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
  10.176                            [old_R, Func (Unit, R2)]))
  10.177       | Func (R1', R2') =>
  10.178         rel_expr_from_rel_expr kk R2 R2' (#kk_project_seq kk r (arity_of_rep R1')
  10.179                                (arity_of_rep R2'))
  10.180 -     | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
  10.181 +     | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
  10.182                         [old_R, Func (Unit, R2)]))
  10.183    | func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r =
  10.184      (case old_R of
  10.185 @@ -592,7 +592,7 @@
  10.186       | Func (R1', Atom (2, j0)) =>
  10.187         func_from_no_opt_rel_expr kk R1 (Formula Neut)
  10.188             (Func (R1', Formula Neut)) (#kk_join kk r (Kodkod.Atom (j0 + 1)))
  10.189 -     | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
  10.190 +     | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
  10.191                         [old_R, Func (R1, Formula Neut)]))
  10.192    | func_from_no_opt_rel_expr kk R1 R2 old_R r =
  10.193      case old_R of
  10.194 @@ -621,7 +621,7 @@
  10.195                                   (#kk_rel_eq kk r2 r3)
  10.196               end
  10.197             end
  10.198 -         | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
  10.199 +         | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
  10.200                             [old_R, Func (R1, R2)]))
  10.201      | Func (Unit, R2') =>
  10.202        let val j0 = some_j0 in
  10.203 @@ -648,7 +648,7 @@
  10.204                                                        (dom_schema @ ran_schema))
  10.205                                 (#kk_subset kk ran_prod app)
  10.206          end
  10.207 -    | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
  10.208 +    | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
  10.209                        [old_R, Func (R1, R2)])
  10.210  (* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  10.211  and rel_expr_from_rel_expr kk new_R old_R r =
  10.212 @@ -657,7 +657,7 @@
  10.213      val unopt_new_R = unopt_rep new_R
  10.214    in
  10.215      if unopt_old_R <> old_R andalso unopt_new_R = new_R then
  10.216 -      raise REP ("NitpickKodkod.rel_expr_from_rel_expr", [old_R, new_R])
  10.217 +      raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R])
  10.218      else if unopt_new_R = unopt_old_R then
  10.219        r
  10.220      else
  10.221 @@ -666,7 +666,7 @@
  10.222         | Struct Rs => struct_from_rel_expr kk Rs
  10.223         | Vect (k, R') => vect_from_rel_expr kk k R'
  10.224         | Func (R1, R2) => func_from_no_opt_rel_expr kk R1 R2
  10.225 -       | _ => raise REP ("NitpickKodkod.rel_expr_from_rel_expr",
  10.226 +       | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr",
  10.227                           [old_R, new_R]))
  10.228            unopt_old_R r
  10.229    end
  10.230 @@ -683,13 +683,13 @@
  10.231      else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (Kodkod.Rel x)
  10.232      else Kodkod.True
  10.233    | declarative_axiom_for_plain_rel _ u =
  10.234 -    raise NUT ("NitpickKodkod.declarative_axiom_for_plain_rel", [u])
  10.235 +    raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
  10.236  
  10.237  (* nut NameTable.table -> styp -> Kodkod.rel_expr * rep * int *)
  10.238  fun const_triple rel_table (x as (s, T)) =
  10.239    case the_name rel_table (ConstName (s, T, Any)) of
  10.240      FreeRel ((n, j), _, R, _) => (Kodkod.Rel (n, j), R, n)
  10.241 -  | _ => raise TERM ("NitpickKodkod.const_triple", [Const x])
  10.242 +  | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
  10.243  
  10.244  (* nut NameTable.table -> styp -> Kodkod.rel_expr *)
  10.245  fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
  10.246 @@ -849,7 +849,8 @@
  10.247                        (~1 upto num_sels - 1)
  10.248      val j0 = case triples |> hd |> #2 of
  10.249                 Func (Atom (_, j0), _) => j0
  10.250 -             | R => raise REP ("NitpickKodkod.uniqueness_axiom_for_constr", [R])
  10.251 +             | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
  10.252 +                               [R])
  10.253      val set_r = triples |> hd |> #1
  10.254    in
  10.255      if num_sels = 0 then
  10.256 @@ -960,7 +961,7 @@
  10.257             let val opt1 = is_opt_rep (rep_of u1) in
  10.258               case polar of
  10.259                 Neut => if opt1 then
  10.260 -                         raise NUT ("NitpickKodkod.to_f (Finite)", [u])
  10.261 +                         raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
  10.262                         else
  10.263                           Kodkod.True
  10.264               | Pos => formula_for_bool (not opt1)
  10.265 @@ -992,7 +993,7 @@
  10.266               if not (is_opt_rep ran_R) then
  10.267                 to_set_bool_op kk_implies kk_subset u1 u2
  10.268               else if polar = Neut then
  10.269 -               raise NUT ("NitpickKodkod.to_f (Subset)", [u])
  10.270 +               raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u])
  10.271               else
  10.272                 let
  10.273                   (* bool -> nut -> Kodkod.rel_expr *)
  10.274 @@ -1102,16 +1103,16 @@
  10.275           | Op3 (If, _, _, u1, u2, u3) =>
  10.276             kk_formula_if (to_f u1) (to_f u2) (to_f u3)
  10.277           | FormulaReg (j, _, _) => Kodkod.FormulaReg j
  10.278 -         | _ => raise NUT ("NitpickKodkod.to_f", [u]))
  10.279 +         | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
  10.280        | Atom (2, j0) => formula_from_atom j0 (to_r u)
  10.281 -      | _ => raise NUT ("NitpickKodkod.to_f", [u])
  10.282 +      | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])
  10.283      (* polarity -> nut -> Kodkod.formula *)
  10.284      and to_f_with_polarity polar u =
  10.285        case rep_of u of
  10.286          Formula _ => to_f u
  10.287        | Atom (2, j0) => formula_from_atom j0 (to_r u)
  10.288        | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u)
  10.289 -      | _ => raise NUT ("NitpickKodkod.to_f_with_polarity", [u])
  10.290 +      | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u])
  10.291      (* nut -> Kodkod.rel_expr *)
  10.292      and to_r u =
  10.293        case u of
  10.294 @@ -1142,12 +1143,12 @@
  10.295        | Cst (Num j, @{typ int}, R) =>
  10.296           (case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
  10.297              ~1 => if is_opt_rep R then Kodkod.None
  10.298 -                  else raise NUT ("NitpickKodkod.to_r (Num)", [u])
  10.299 +                  else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
  10.300            | j' => Kodkod.Atom j')
  10.301        | Cst (Num j, T, R) =>
  10.302          if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
  10.303          else if is_opt_rep R then Kodkod.None
  10.304 -        else raise NUT ("NitpickKodkod.to_r", [u])
  10.305 +        else raise NUT ("Nitpick_Kodkod.to_r", [u])
  10.306        | Cst (Unknown, _, R) => empty_rel_for_rep R
  10.307        | Cst (Unrep, _, R) => empty_rel_for_rep R
  10.308        | Cst (Suc, T, Func (Atom x, _)) =>
  10.309 @@ -1177,7 +1178,7 @@
  10.310                (kk_product (Kodkod.AtomSeq (max_int_for_card int_k + 1, nat_j0))
  10.311                            Kodkod.Univ)
  10.312          else
  10.313 -          raise BAD ("NitpickKodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
  10.314 +          raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
  10.315        | Cst (IntToNat, _, Func (Atom (int_k, int_j0), nat_R)) =>
  10.316          let
  10.317            val abs_card = max_int_for_card int_k + 1
  10.318 @@ -1192,7 +1193,7 @@
  10.319                            (kk_product (Kodkod.AtomSeq (overlap, int_j0))
  10.320                                        Kodkod.Univ))
  10.321            else
  10.322 -            raise BAD ("NitpickKodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
  10.323 +            raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
  10.324          end
  10.325        | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
  10.326        | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None
  10.327 @@ -1204,10 +1205,10 @@
  10.328                Func (Struct [R1, R2], _) => (R1, R2)
  10.329              | Func (R1, _) =>
  10.330                if card_of_rep R1 <> 1 then
  10.331 -                raise REP ("NitpickKodkod.to_r (Converse)", [R])
  10.332 +                raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
  10.333                else
  10.334                  pairself (Atom o pair 1 o offset_of_type ofs) (b_T, a_T)
  10.335 -            | _ => raise REP ("NitpickKodkod.to_r (Converse)", [R])
  10.336 +            | _ => raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
  10.337            val body_R = body_rep R
  10.338            val a_arity = arity_of_rep a_R
  10.339            val b_arity = arity_of_rep b_R
  10.340 @@ -1257,7 +1258,7 @@
  10.341                              (rel_expr_to_func kk R1 bool_atom_R
  10.342                                                (Func (R1, Formula Neut)) r))
  10.343                 (to_opt R1 u1)
  10.344 -         | _ => raise NUT ("NitpickKodkod.to_r (SingletonSet)", [u]))
  10.345 +         | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u]))
  10.346        | Op1 (Tha, T, R, u1) =>
  10.347          if is_opt_rep R then
  10.348            kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
  10.349 @@ -1384,7 +1385,7 @@
  10.350                   kk_product (kk_join (do_nut r a_R b_R u2)
  10.351                                       (do_nut r b_R c_R u1)) r
  10.352               in kk_union (do_term true_atom) (do_term false_atom) end
  10.353 -           | _ => raise NUT ("NitpickKodkod.to_r (Composition)", [u]))
  10.354 +           | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
  10.355            |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
  10.356          end
  10.357        | Op2 (Product, T, R, u1, u2) =>
  10.358 @@ -1408,7 +1409,7 @@
  10.359                 fun do_term r =
  10.360                   kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
  10.361               in kk_union (do_term true_atom) (do_term false_atom) end
  10.362 -           | _ => raise NUT ("NitpickKodkod.to_r (Product)", [u]))
  10.363 +           | _ => raise NUT ("Nitpick_Kodkod.to_r (Product)", [u]))
  10.364            |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, b_R], body_R))
  10.365          end
  10.366        | Op2 (Image, T, R, u1, u2) =>
  10.367 @@ -1437,8 +1438,8 @@
  10.368                   rel_expr_from_rel_expr kk R core_R core_r
  10.369               end
  10.370             else
  10.371 -             raise NUT ("NitpickKodkod.to_r (Image)", [u1, u2])
  10.372 -         | _ => raise NUT ("NitpickKodkod.to_r (Image)", [u1, u2]))
  10.373 +             raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])
  10.374 +         | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]))
  10.375        | Op2 (Apply, @{typ nat}, _,
  10.376               Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
  10.377          if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
  10.378 @@ -1492,7 +1493,7 @@
  10.379              | us' =>
  10.380                kk_rel_if (kk_some (fold1 kk_product (map to_r us')))
  10.381                          (Kodkod.Atom j0) Kodkod.None)
  10.382 -         | _ => raise NUT ("NitpickKodkod.to_r (Tuple)", [u]))
  10.383 +         | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
  10.384        | Construct ([u'], _, _, []) => to_r u'
  10.385        | Construct (_ :: sel_us, T, R, arg_us) =>
  10.386          let
  10.387 @@ -1516,23 +1517,23 @@
  10.388        | BoundRel (x, _, _, _) => Kodkod.Var x
  10.389        | FreeRel (x, _, _, _) => Kodkod.Rel x
  10.390        | RelReg (j, _, R) => Kodkod.RelReg (arity_of_rep R, j)
  10.391 -      | u => raise NUT ("NitpickKodkod.to_r", [u])
  10.392 +      | u => raise NUT ("Nitpick_Kodkod.to_r", [u])
  10.393      (* nut -> Kodkod.decl *)
  10.394      and to_decl (BoundRel (x, _, R, _)) =
  10.395          Kodkod.DeclOne (x, Kodkod.AtomSeq (the_single (atom_schema_of_rep R)))
  10.396 -      | to_decl u = raise NUT ("NitpickKodkod.to_decl", [u])
  10.397 +      | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
  10.398      (* nut -> Kodkod.expr_assign *)
  10.399      and to_expr_assign (FormulaReg (j, _, R)) u =
  10.400          Kodkod.AssignFormulaReg (j, to_f u)
  10.401        | to_expr_assign (RelReg (j, _, R)) u =
  10.402          Kodkod.AssignRelReg ((arity_of_rep R, j), to_r u)
  10.403 -      | to_expr_assign u1 _ = raise NUT ("NitpickKodkod.to_expr_assign", [u1])
  10.404 +      | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
  10.405      (* int * int -> nut -> Kodkod.rel_expr *)
  10.406      and to_atom (x as (k, j0)) u =
  10.407        case rep_of u of
  10.408          Formula _ => atom_from_formula kk j0 (to_f u)
  10.409        | Unit => if k = 1 then Kodkod.Atom j0
  10.410 -                else raise NUT ("NitpickKodkod.to_atom", [u])
  10.411 +                else raise NUT ("Nitpick_Kodkod.to_atom", [u])
  10.412        | R => atom_from_rel_expr kk x R (to_r u)
  10.413      (* rep list -> nut -> Kodkod.rel_expr *)
  10.414      and to_struct Rs u =
  10.415 @@ -1563,7 +1564,7 @@
  10.416        | to_rep (Vect (k, R)) u = to_vect k R u
  10.417        | to_rep (Func (R1, R2)) u = to_func R1 R2 u
  10.418        | to_rep (Opt R) u = to_opt R u
  10.419 -      | to_rep R _ = raise REP ("NitpickKodkod.to_rep", [R])
  10.420 +      | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R])
  10.421      (* nut -> Kodkod.rel_expr *)
  10.422      and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u
  10.423      (* nut list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
  10.424 @@ -1593,7 +1594,7 @@
  10.425      (* rep list -> nut list -> Kodkod.rel_expr *)
  10.426      and to_product Rs us =
  10.427        case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of
  10.428 -        [] => raise REP ("NitpickKodkod.to_product", Rs)
  10.429 +        [] => raise REP ("Nitpick_Kodkod.to_product", Rs)
  10.430        | rs => fold1 kk_product rs
  10.431      (* int -> typ -> rep -> nut -> Kodkod.rel_expr *)
  10.432      and to_nth_pair_sel n res_T res_R u =
  10.433 @@ -1639,7 +1640,7 @@
  10.434            connective (formula_from_atom j0 r1) (formula_from_atom j0 r2)
  10.435          | Func (R1, Atom _) => set_oper (kk_join r1 true_atom)
  10.436                                          (kk_join r2 true_atom)
  10.437 -        | _ => raise REP ("NitpickKodkod.to_set_bool_op", [min_R])
  10.438 +        | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
  10.439        end
  10.440      (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula)
  10.441         -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
  10.442 @@ -1676,7 +1677,7 @@
  10.443                                                                  neg_second)))
  10.444                                  false_atom))
  10.445                     r1 r2
  10.446 -             | _ => raise REP ("NitpickKodkod.to_set_op", [min_R]))
  10.447 +             | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
  10.448        end
  10.449      (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *)
  10.450      and to_apply res_R func_u arg_u =
  10.451 @@ -1713,7 +1714,7 @@
  10.452          rel_expr_from_rel_expr kk res_R R2
  10.453              (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
  10.454          |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
  10.455 -      | _ => raise NUT ("NitpickKodkod.to_apply", [func_u])
  10.456 +      | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])
  10.457      (* int -> rep -> rep -> Kodkod.rel_expr -> nut *)
  10.458      and to_apply_vect k R' res_R func_r arg_u =
  10.459        let
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 27 12:16:26 2009 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 27 14:40:24 2009 +0100
    11.3 @@ -7,9 +7,9 @@
    11.4  
    11.5  signature NITPICK_MODEL =
    11.6  sig
    11.7 -  type scope = NitpickScope.scope
    11.8 -  type rep = NitpickRep.rep
    11.9 -  type nut = NitpickNut.nut
   11.10 +  type scope = Nitpick_Scope.scope
   11.11 +  type rep = Nitpick_Rep.rep
   11.12 +  type nut = Nitpick_Nut.nut
   11.13  
   11.14    type params = {
   11.15      show_skolems: bool,
   11.16 @@ -29,15 +29,15 @@
   11.17      -> Kodkod.raw_bound list -> term -> bool option
   11.18  end;
   11.19  
   11.20 -structure NitpickModel : NITPICK_MODEL =
   11.21 +structure Nitpick_Model : NITPICK_MODEL =
   11.22  struct
   11.23  
   11.24 -open NitpickUtil
   11.25 -open NitpickHOL
   11.26 -open NitpickScope
   11.27 -open NitpickPeephole
   11.28 -open NitpickRep
   11.29 -open NitpickNut
   11.30 +open Nitpick_Util
   11.31 +open Nitpick_HOL
   11.32 +open Nitpick_Scope
   11.33 +open Nitpick_Peephole
   11.34 +open Nitpick_Rep
   11.35 +open Nitpick_Nut
   11.36  
   11.37  type params = {
   11.38    show_skolems: bool,
   11.39 @@ -57,7 +57,7 @@
   11.40      prefix ^ substring (short_name s, 0, 1) ^ nat_subscript (j + 1)
   11.41    | atom_name prefix (T as TFree (s, _)) j =
   11.42      prefix ^ perhaps (try (unprefix "'")) s ^ nat_subscript (j + 1)
   11.43 -  | atom_name _ T _ = raise TYPE ("NitpickModel.atom_name", [T], [])
   11.44 +  | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
   11.45  (* bool -> typ -> int -> term *)
   11.46  fun atom for_auto T j =
   11.47    if for_auto then
   11.48 @@ -130,7 +130,7 @@
   11.49      fun aux (Const (s, _)) = (s <> non_opt_name, ([], []))
   11.50        | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
   11.51          let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end
   11.52 -      | aux t = raise TERM ("NitpickModel.dest_plain_fun", [t])
   11.53 +      | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
   11.54    in apsnd (pairself rev) o aux end
   11.55  
   11.56  (* typ -> term -> term list * term *)
   11.57 @@ -138,7 +138,7 @@
   11.58                   (Const (@{const_name Pair}, _) $ t1 $ t2) =
   11.59      break_in_two T2 t2 |>> cons t1
   11.60    | break_in_two _ (Const (@{const_name Pair}, _) $ t1 $ t2) = ([t1], t2)
   11.61 -  | break_in_two _ t = raise TERM ("NitpickModel.break_in_two", [t])
   11.62 +  | break_in_two _ t = raise TERM ("Nitpick_Model.break_in_two", [t])
   11.63  (* typ -> term -> term -> term *)
   11.64  fun pair_up (Type ("*", [T1', T2']))
   11.65              (t1 as Const (@{const_name Pair},
   11.66 @@ -180,7 +180,7 @@
   11.67                   [T1' --> T2', T1', T2'] ---> T1' --> T2')
   11.68            $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
   11.69          | do_arrow _ _ _ _ t =
   11.70 -          raise TERM ("NitpickModel.typecast_fun.do_arrow", [t])
   11.71 +          raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t])
   11.72        and do_fun T1' T2' T1 T2 t =
   11.73          case factor_out_types T1' T1 of
   11.74            ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
   11.75 @@ -188,7 +188,7 @@
   11.76            t |> do_curry T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
   11.77          | ((T1a', SOME T1b'), (_, NONE)) =>
   11.78            t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
   11.79 -        | _ => raise TYPE ("NitpickModel.typecast_fun.do_fun", [T1, T1'], [])
   11.80 +        | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
   11.81        (* typ -> typ -> term -> term *)
   11.82        and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t =
   11.83            do_fun T1' T2' T1 T2 t
   11.84 @@ -198,9 +198,9 @@
   11.85            $ do_term T1' T1 t1 $ do_term T2' T2 t2
   11.86          | do_term T' T t =
   11.87            if T = T' then t
   11.88 -          else raise TYPE ("NitpickModel.typecast_fun.do_term", [T, T'], [])
   11.89 +          else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], [])
   11.90      in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
   11.91 -  | typecast_fun T' _ _ _ = raise TYPE ("NitpickModel.typecast_fun", [T'], [])
   11.92 +  | typecast_fun T' _ _ _ = raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
   11.93  
   11.94  (* term -> string *)
   11.95  fun truth_const_sort_key @{const True} = "0"
   11.96 @@ -302,7 +302,7 @@
   11.97            term_for_rep seen T T' (Vect (k1, Atom (k2, 0)))
   11.98                         [nth_combination (replicate k1 (k2, 0)) j]
   11.99            handle General.Subscript =>
  11.100 -                 raise ARG ("NitpickModel.reconstruct_term.term_for_atom",
  11.101 +                 raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
  11.102                              signed_string_of_int j ^ " for " ^
  11.103                              string_for_rep (Vect (k1, Atom (k2, 0))))
  11.104          end
  11.105 @@ -350,7 +350,7 @@
  11.106                map (fn x => get_first
  11.107                                 (fn ConstName (s', T', R) =>
  11.108                                     if (s', T') = x then SOME R else NONE
  11.109 -                                 | u => raise NUT ("NitpickModel.reconstruct_\
  11.110 +                                 | u => raise NUT ("Nitpick_Model.reconstruct_\
  11.111                                                     \term.term_for_atom", [u]))
  11.112                                 sel_names |> the) sel_xs
  11.113              val arg_Rs = map (snd o dest_Func) sel_Rs
  11.114 @@ -389,7 +389,7 @@
  11.115                                   | n2 => Const (@{const_name HOL.divide},
  11.116                                                  [num_T, num_T] ---> num_T)
  11.117                                           $ mk_num n1 $ mk_num n2)
  11.118 -                      | _ => raise TERM ("NitpickModel.reconstruct_term.term_\
  11.119 +                      | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
  11.120                                           \for_atom (Abs_Frac)", ts)
  11.121                      end
  11.122                    else if not for_auto andalso is_abs_fun thy constr_x then
  11.123 @@ -421,7 +421,7 @@
  11.124      and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0
  11.125        | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
  11.126          if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0)
  11.127 -        else raise REP ("NitpickModel.reconstruct_term.term_for_rep", [R])
  11.128 +        else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
  11.129        | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
  11.130          let
  11.131            val arity1 = arity_of_rep R1
  11.132 @@ -454,7 +454,7 @@
  11.133        | term_for_rep seen T T' (Opt R) jss =
  11.134          if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
  11.135        | term_for_rep seen T _ R jss =
  11.136 -        raise ARG ("NitpickModel.reconstruct_term.term_for_rep",
  11.137 +        raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
  11.138                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
  11.139                     string_of_int (length jss))
  11.140    in
  11.141 @@ -576,7 +576,7 @@
  11.142              (assign_operator_for_const (s, T),
  11.143               user_friendly_const ext_ctxt (base_name, step_name) formats (s, T),
  11.144               T)
  11.145 -          | _ => raise NUT ("NitpickModel.reconstruct_hol_model.\
  11.146 +          | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
  11.147                              \pretty_for_assign", [name])
  11.148          val t2 = if rep_of name = Any then
  11.149                     Const (@{const_name undefined}, T')
  11.150 @@ -601,7 +601,7 @@
  11.151      fun integer_datatype T =
  11.152        [{typ = T, card = card_of_type card_assigns T, co = false,
  11.153          precise = false, constrs = []}]
  11.154 -      handle TYPE ("NitpickHOL.card_of_type", _, _) => []
  11.155 +      handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
  11.156      val (codatatypes, datatypes) =
  11.157        List.partition #co datatypes
  11.158        ||> append (integer_datatype nat_T @ integer_datatype int_T)
  11.159 @@ -637,7 +637,7 @@
  11.160                            free_names of
  11.161                  [name] => name
  11.162                | [] => FreeName (s, T, Any)
  11.163 -              | _ => raise TERM ("NitpickModel.reconstruct_hol_model",
  11.164 +              | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
  11.165                                   [Const x])) all_frees
  11.166      val chunks = block_of_names true "Free variable" free_names @
  11.167                   block_of_names show_skolems "Skolem constant" skolem_names @
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Oct 27 12:16:26 2009 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Oct 27 14:40:24 2009 +0100
    12.3 @@ -7,17 +7,17 @@
    12.4  
    12.5  signature NITPICK_MONO =
    12.6  sig
    12.7 -  type extended_context = NitpickHOL.extended_context
    12.8 +  type extended_context = Nitpick_HOL.extended_context
    12.9  
   12.10    val formulas_monotonic :
   12.11      extended_context -> typ -> term list -> term list -> term -> bool
   12.12  end;
   12.13  
   12.14 -structure NitpickMono : NITPICK_MONO =
   12.15 +structure Nitpick_Mono : NITPICK_MONO =
   12.16  struct
   12.17  
   12.18 -open NitpickUtil
   12.19 -open NitpickHOL
   12.20 +open Nitpick_Util
   12.21 +open Nitpick_HOL
   12.22  
   12.23  type var = int
   12.24  
   12.25 @@ -363,11 +363,11 @@
   12.26                    accum =
   12.27      (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
   12.28       handle Library.UnequalLengths =>
   12.29 -            raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2]))
   12.30 +            raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
   12.31    | do_ctype_comp cmp xs (CType _) (CType _) accum =
   12.32      accum (* no need to compare them thanks to the cache *)
   12.33    | do_ctype_comp _ _ C1 C2 _ =
   12.34 -    raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2])
   12.35 +    raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
   12.36  
   12.37  (* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *)
   12.38  fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
   12.39 @@ -413,7 +413,7 @@
   12.40    | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
   12.41      accum |> fold (do_notin_ctype_fv sn sexp) Cs
   12.42    | do_notin_ctype_fv _ _ C _ =
   12.43 -    raise CTYPE ("NitpickMono.do_notin_ctype_fv", [C])
   12.44 +    raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C])
   12.45  
   12.46  (* sign -> ctype -> constraint_set -> constraint_set *)
   12.47  fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
   12.48 @@ -584,13 +584,13 @@
   12.49        case ctype_for (nth_range_type 2 T) of
   12.50          C as CPair (a_C, b_C) =>
   12.51          (CFun (a_C, S Neg, CFun (b_C, S Neg, C)), accum)
   12.52 -      | C => raise CTYPE ("NitpickMono.consider_term.do_pair_constr", [C])
   12.53 +      | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
   12.54      (* int -> typ -> accumulator -> ctype * accumulator *)
   12.55      fun do_nth_pair_sel n T =
   12.56        case ctype_for (domain_type T) of
   12.57          C as CPair (a_C, b_C) =>
   12.58          pair (CFun (C, S Neg, if n = 0 then a_C else b_C))
   12.59 -      | C => raise CTYPE ("NitpickMono.consider_term.do_nth_pair_sel", [C])
   12.60 +      | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
   12.61      val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
   12.62      (* typ -> term -> accumulator -> ctype * accumulator *)
   12.63      fun do_bounded_quantifier abs_T bound_t body_t accum =
   12.64 @@ -770,7 +770,7 @@
   12.65               | _ => case C1 of
   12.66                        CFun (C11, _, C12) =>
   12.67                        (C12, accum ||> add_is_sub_ctype C2 C11)
   12.68 -                    | _ => raise CTYPE ("NitpickMono.consider_term.do_term \
   12.69 +                    | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \
   12.70                                          \(op $)", [C1])
   12.71             end)
   12.72          |> tap (fn (C, _) =>
   12.73 @@ -906,7 +906,7 @@
   12.74            | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum
   12.75            | @{const "op &"} $ t1 $ t2 => accum |> do_formula t1 |> do_formula t2
   12.76            | @{const "op -->"} $ t1 $ t2 => do_implies t1 t2 accum
   12.77 -          | _ => raise TERM ("NitpickMono.consider_definitional_axiom.\
   12.78 +          | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
   12.79                               \do_formula", [t])
   12.80      in do_formula t end
   12.81  
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Oct 27 12:16:26 2009 +0100
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Oct 27 14:40:24 2009 +0100
    13.3 @@ -7,11 +7,11 @@
    13.4  
    13.5  signature NITPICK_NUT =
    13.6  sig
    13.7 -  type special_fun = NitpickHOL.special_fun
    13.8 -  type extended_context = NitpickHOL.extended_context
    13.9 -  type scope = NitpickScope.scope
   13.10 -  type name_pool = NitpickPeephole.name_pool
   13.11 -  type rep = NitpickRep.rep
   13.12 +  type special_fun = Nitpick_HOL.special_fun
   13.13 +  type extended_context = Nitpick_HOL.extended_context
   13.14 +  type scope = Nitpick_Scope.scope
   13.15 +  type name_pool = Nitpick_Peephole.name_pool
   13.16 +  type rep = Nitpick_Rep.rep
   13.17  
   13.18    datatype cst =
   13.19      Unity |
   13.20 @@ -121,14 +121,14 @@
   13.21    val rename_vars_in_nut : name_pool -> nut NameTable.table -> nut -> nut
   13.22  end;
   13.23  
   13.24 -structure NitpickNut : NITPICK_NUT =
   13.25 +structure Nitpick_Nut : NITPICK_NUT =
   13.26  struct
   13.27  
   13.28 -open NitpickUtil
   13.29 -open NitpickHOL
   13.30 -open NitpickScope
   13.31 -open NitpickPeephole
   13.32 -open NitpickRep
   13.33 +open Nitpick_Util
   13.34 +open Nitpick_HOL
   13.35 +open Nitpick_Scope
   13.36 +open Nitpick_Peephole
   13.37 +open Nitpick_Rep
   13.38  
   13.39  datatype cst =
   13.40    Unity |
   13.41 @@ -357,16 +357,16 @@
   13.42    | nickname_of (ConstName (s, _, _)) = s
   13.43    | nickname_of (BoundRel (_, _, _, nick)) = nick
   13.44    | nickname_of (FreeRel (_, _, _, nick)) = nick
   13.45 -  | nickname_of u = raise NUT ("NitpickNut.nickname_of", [u])
   13.46 +  | nickname_of u = raise NUT ("Nitpick_Nut.nickname_of", [u])
   13.47  
   13.48  (* nut -> bool *)
   13.49  fun is_skolem_name u =
   13.50    space_explode name_sep (nickname_of u)
   13.51    |> exists (String.isPrefix skolem_prefix)
   13.52 -  handle NUT ("NitpickNut.nickname_of", _) => false
   13.53 +  handle NUT ("Nitpick_Nut.nickname_of", _) => false
   13.54  fun is_eval_name u =
   13.55    String.isPrefix eval_prefix (nickname_of u)
   13.56 -  handle NUT ("NitpickNut.nickname_of", _) => false
   13.57 +  handle NUT ("Nitpick_Nut.nickname_of", _) => false
   13.58  (* cst -> nut -> bool *)
   13.59  fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
   13.60    | is_Cst _ _ = false
   13.61 @@ -407,7 +407,7 @@
   13.62      (case fast_string_ord (s1, s2) of
   13.63         EQUAL => TermOrd.typ_ord (T1, T2)
   13.64       | ord => ord)
   13.65 -  | name_ord (u1, u2) = raise NUT ("NitpickNut.name_ord", [u1, u2])
   13.66 +  | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2])
   13.67  
   13.68  (* nut -> nut -> int *)
   13.69  fun num_occs_in_nut needle_u stack_u =
   13.70 @@ -430,7 +430,7 @@
   13.71  fun modify_name_rep (BoundName (j, T, _, nick)) R = BoundName (j, T, R, nick)
   13.72    | modify_name_rep (FreeName (s, T, _)) R = FreeName (s, T, R)
   13.73    | modify_name_rep (ConstName (s, T, _)) R = ConstName (s, T, R)
   13.74 -  | modify_name_rep u _ = raise NUT ("NitpickNut.modify_name_rep", [u])
   13.75 +  | modify_name_rep u _ = raise NUT ("Nitpick_Nut.modify_name_rep", [u])
   13.76  
   13.77  structure NameTable = Table(type key = nut val ord = name_ord)
   13.78  
   13.79 @@ -438,12 +438,12 @@
   13.80  fun the_name table name =
   13.81    case NameTable.lookup table name of
   13.82      SOME u => u
   13.83 -  | NONE => raise NUT ("NitpickNut.the_name", [name])
   13.84 +  | NONE => raise NUT ("Nitpick_Nut.the_name", [name])
   13.85  (* nut NameTable.table -> nut -> Kodkod.n_ary_index *)
   13.86  fun the_rel table name =
   13.87    case the_name table name of
   13.88      FreeRel (x, _, _, _) => x
   13.89 -  | u => raise NUT ("NitpickNut.the_rel", [u])
   13.90 +  | u => raise NUT ("Nitpick_Nut.the_rel", [u])
   13.91  
   13.92  (* typ * term -> typ * term *)
   13.93  fun mk_fst (_, Const (@{const_name Pair}, T) $ t1 $ _) = (domain_type T, t1)
   13.94 @@ -669,13 +669,13 @@
   13.95              (case arity_of_built_in_const fast_descrs x of
   13.96                 SOME n =>
   13.97                 (case n - length ts of
   13.98 -                  0 => raise TERM ("NitpickNut.nut_from_term.aux", [t])
   13.99 +                  0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
  13.100                  | k => if k > 0 then sub (eta_expand Ts t k)
  13.101                         else do_apply t0 ts)
  13.102               | NONE => if null ts then ConstName (s, T, Any)
  13.103                         else do_apply t0 ts)
  13.104          | (Free (s, T), []) => FreeName (s, T, Any)
  13.105 -        | (Var _, []) => raise TERM ("NitpickNut.nut_from_term", [t])
  13.106 +        | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term", [t])
  13.107          | (Bound j, []) =>
  13.108            BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
  13.109          | (Abs (s, T, t1), []) =>
  13.110 @@ -1106,7 +1106,7 @@
  13.111                   else
  13.112                     unopt_rep R
  13.113               in s_op2 Lambda T R u1' u2' end
  13.114 -           | R => raise NUT ("NitpickNut.aux.choose_reps_in_nut", [u]))
  13.115 +           | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
  13.116          | Op2 (oper, T, _, u1, u2) =>
  13.117            if oper mem [All, Exist] then
  13.118              let
  13.119 @@ -1274,9 +1274,9 @@
  13.120    | shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
  13.121      Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
  13.122    | shape_tuple T R [u] =
  13.123 -    if type_of u = T then u else raise NUT ("NitpickNut.shape_tuple", [u])
  13.124 +    if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
  13.125    | shape_tuple T Unit [] = Cst (Unity, T, Unit)
  13.126 -  | shape_tuple _ _ us = raise NUT ("NitpickNut.shape_tuple", us)
  13.127 +  | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
  13.128  
  13.129  (* bool -> nut -> nut list * name_pool * nut NameTable.table
  13.130     -> nut list * name_pool * nut NameTable.table *)
    14.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Tue Oct 27 12:16:26 2009 +0100
    14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Tue Oct 27 14:40:24 2009 +0100
    14.3 @@ -86,11 +86,11 @@
    14.4    val kodkod_constrs : bool -> int -> int -> int -> kodkod_constrs
    14.5  end;
    14.6  
    14.7 -structure NitpickPeephole : NITPICK_PEEPHOLE =
    14.8 +structure Nitpick_Peephole : NITPICK_PEEPHOLE =
    14.9  struct
   14.10  
   14.11  open Kodkod
   14.12 -open NitpickUtil
   14.13 +open Nitpick_Util
   14.14  
   14.15  type name_pool = {
   14.16    rels: n_ary_index list,
   14.17 @@ -188,20 +188,20 @@
   14.18      if is_none_product r1 orelse is_none_product r2 then SOME false else NONE
   14.19  
   14.20  (* int -> rel_expr *)
   14.21 -fun empty_n_ary_rel 0 = raise ARG ("NitpickPeephole.empty_n_ary_rel", "0")
   14.22 +fun empty_n_ary_rel 0 = raise ARG ("Nitpick_Peephole.empty_n_ary_rel", "0")
   14.23    | empty_n_ary_rel n = funpow (n - 1) (curry Product None) None
   14.24  
   14.25  (* decl -> rel_expr *)
   14.26  fun decl_one_set (DeclOne (_, r)) = r
   14.27    | decl_one_set _ =
   14.28 -    raise ARG ("NitpickPeephole.decl_one_set", "not \"DeclOne\"")
   14.29 +    raise ARG ("Nitpick_Peephole.decl_one_set", "not \"DeclOne\"")
   14.30  
   14.31  (* int_expr -> bool *)
   14.32  fun is_Num (Num _) = true
   14.33    | is_Num _ = false
   14.34  (* int_expr -> int *)
   14.35  fun dest_Num (Num k) = k
   14.36 -  | dest_Num _ = raise ARG ("NitpickPeephole.dest_Num", "not \"Num\"")
   14.37 +  | dest_Num _ = raise ARG ("Nitpick_Peephole.dest_Num", "not \"Num\"")
   14.38  (* int -> int -> int_expr list *)
   14.39  fun num_seq j0 n = map Num (index_seq j0 n)
   14.40  
    15.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Oct 27 12:16:26 2009 +0100
    15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Oct 27 14:40:24 2009 +0100
    15.3 @@ -7,8 +7,8 @@
    15.4  
    15.5  signature NITPICK_REP =
    15.6  sig
    15.7 -  type polarity = NitpickUtil.polarity
    15.8 -  type scope = NitpickScope.scope
    15.9 +  type polarity = Nitpick_Util.polarity
   15.10 +  type scope = Nitpick_Scope.scope
   15.11  
   15.12    datatype rep =
   15.13      Any |
   15.14 @@ -58,12 +58,12 @@
   15.15    val all_combinations_for_reps : rep list -> int list list
   15.16  end;
   15.17  
   15.18 -structure NitpickRep : NITPICK_REP =
   15.19 +structure Nitpick_Rep : NITPICK_REP =
   15.20  struct
   15.21  
   15.22 -open NitpickUtil
   15.23 -open NitpickHOL
   15.24 -open NitpickScope
   15.25 +open Nitpick_Util
   15.26 +open Nitpick_HOL
   15.27 +open Nitpick_Scope
   15.28  
   15.29  datatype rep =
   15.30    Any |
   15.31 @@ -111,7 +111,7 @@
   15.32    | is_opt_rep _ = false
   15.33  
   15.34  (* rep -> int *)
   15.35 -fun card_of_rep Any = raise REP ("NitpickRep.card_of_rep", [Any])
   15.36 +fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any])
   15.37    | card_of_rep (Formula _) = 2
   15.38    | card_of_rep Unit = 1
   15.39    | card_of_rep (Atom (k, _)) = k
   15.40 @@ -120,7 +120,7 @@
   15.41    | card_of_rep (Func (R1, R2)) =
   15.42      reasonable_power (card_of_rep R2) (card_of_rep R1)
   15.43    | card_of_rep (Opt R) = card_of_rep R
   15.44 -fun arity_of_rep Any = raise REP ("NitpickRep.arity_of_rep", [Any])
   15.45 +fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any])
   15.46    | arity_of_rep (Formula _) = 0
   15.47    | arity_of_rep Unit = 0
   15.48    | arity_of_rep (Atom _) = 1
   15.49 @@ -129,7 +129,7 @@
   15.50    | arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2
   15.51    | arity_of_rep (Opt R) = arity_of_rep R
   15.52  fun min_univ_card_of_rep Any =
   15.53 -    raise REP ("NitpickRep.min_univ_card_of_rep", [Any])
   15.54 +    raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any])
   15.55    | min_univ_card_of_rep (Formula _) = 0
   15.56    | min_univ_card_of_rep Unit = 0
   15.57    | min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1
   15.58 @@ -151,7 +151,7 @@
   15.59  
   15.60  (* rep -> rep * rep *)
   15.61  fun dest_Func (Func z) = z
   15.62 -  | dest_Func R = raise REP ("NitpickRep.dest_Func", [R])
   15.63 +  | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
   15.64  (* int Typtab.table -> typ -> (unit -> int) -> rep -> rep *)
   15.65  fun smart_range_rep _ _ _ Unit = Unit
   15.66    | smart_range_rep _ _ _ (Vect (_, R)) = R
   15.67 @@ -162,7 +162,7 @@
   15.68      Atom (1, offset_of_type ofs T2)
   15.69    | smart_range_rep ofs (Type ("fun", [_, T2])) ran_card (Atom _) =
   15.70      Atom (ran_card (), offset_of_type ofs T2)
   15.71 -  | smart_range_rep _ _ _ R = raise REP ("NitpickRep.smart_range_rep", [R])
   15.72 +  | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R])
   15.73  
   15.74  (* rep -> rep list *)
   15.75  fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
   15.76 @@ -177,7 +177,7 @@
   15.77    | flip_rep_polarity R = R
   15.78  
   15.79  (* int Typtab.table -> rep -> rep *)
   15.80 -fun one_rep _ _ Any = raise REP ("NitpickRep.one_rep", [Any])
   15.81 +fun one_rep _ _ Any = raise REP ("Nitpick_Rep.one_rep", [Any])
   15.82    | one_rep _ _ (Atom x) = Atom x
   15.83    | one_rep _ _ (Struct Rs) = Struct Rs
   15.84    | one_rep _ _ (Vect z) = Vect z
   15.85 @@ -203,7 +203,7 @@
   15.86    else if polar2 = Neut then
   15.87      polar1
   15.88    else
   15.89 -    raise ARG ("NitpickRep.min_polarity",
   15.90 +    raise ARG ("Nitpick_Rep.min_polarity",
   15.91                 commas (map (quote o string_for_polarity) [polar1, polar2]))
   15.92  
   15.93  (* It's important that Func is before Vect, because if the range is Opt we
   15.94 @@ -236,7 +236,7 @@
   15.95      if k1 < k2 then Vect (k1, R1)
   15.96      else if k1 > k2 then Vect (k2, R2)
   15.97      else Vect (k1, min_rep R1 R2)
   15.98 -  | min_rep R1 R2 = raise REP ("NitpickRep.min_rep", [R1, R2])
   15.99 +  | min_rep R1 R2 = raise REP ("Nitpick_Rep.min_rep", [R1, R2])
  15.100  (* rep list -> rep list -> rep list *)
  15.101  and min_reps [] _ = []
  15.102    | min_reps _ [] = []
  15.103 @@ -253,7 +253,7 @@
  15.104    | Vect (k, _) => k
  15.105    | Func (R1, _) => card_of_rep R1
  15.106    | Opt R => card_of_domain_from_rep ran_card R
  15.107 -  | _ => raise REP ("NitpickRep.card_of_domain_from_rep", [R])
  15.108 +  | _ => raise REP ("Nitpick_Rep.card_of_domain_from_rep", [R])
  15.109  
  15.110  (* int Typtab.table -> typ -> rep -> rep *)
  15.111  fun rep_to_binary_rel_rep ofs T R =
  15.112 @@ -306,10 +306,10 @@
  15.113      (optable_rep ofs T1 (best_one_rep_for_type scope T1),
  15.114       optable_rep ofs T2 (best_one_rep_for_type scope T2))
  15.115    | best_non_opt_symmetric_reps_for_fun_type _ T =
  15.116 -    raise TYPE ("NitpickRep.best_non_opt_symmetric_reps_for_fun_type", [T], [])
  15.117 +    raise TYPE ("Nitpick_Rep.best_non_opt_symmetric_reps_for_fun_type", [T], [])
  15.118  
  15.119  (* rep -> (int * int) list *)
  15.120 -fun atom_schema_of_rep Any = raise REP ("NitpickRep.atom_schema_of_rep", [Any])
  15.121 +fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any])
  15.122    | atom_schema_of_rep (Formula _) = []
  15.123    | atom_schema_of_rep Unit = []
  15.124    | atom_schema_of_rep (Atom x) = [x]
  15.125 @@ -332,7 +332,7 @@
  15.126    | type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) =
  15.127      type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
  15.128    | type_schema_of_rep T (Opt R) = type_schema_of_rep T R
  15.129 -  | type_schema_of_rep T R = raise REP ("NitpickRep.type_schema_of_rep", [R])
  15.130 +  | type_schema_of_rep T R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
  15.131  (* typ list -> rep list -> typ list *)
  15.132  and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs)
  15.133  
    16.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Oct 27 12:16:26 2009 +0100
    16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Oct 27 14:40:24 2009 +0100
    16.3 @@ -7,7 +7,7 @@
    16.4  
    16.5  signature NITPICK_SCOPE =
    16.6  sig
    16.7 -  type extended_context = NitpickHOL.extended_context
    16.8 +  type extended_context = Nitpick_HOL.extended_context
    16.9  
   16.10    type constr_spec = {
   16.11      const: styp,
   16.12 @@ -47,11 +47,11 @@
   16.13      -> int list -> typ list -> typ list -> scope list
   16.14  end;
   16.15  
   16.16 -structure NitpickScope : NITPICK_SCOPE =
   16.17 +structure Nitpick_Scope : NITPICK_SCOPE =
   16.18  struct
   16.19  
   16.20 -open NitpickUtil
   16.21 -open NitpickHOL
   16.22 +open Nitpick_Util
   16.23 +open Nitpick_HOL
   16.24  
   16.25  type constr_spec = {
   16.26    const: styp,
   16.27 @@ -85,7 +85,7 @@
   16.28    List.find (equal T o #typ) dtypes
   16.29  
   16.30  (* dtype_spec list -> styp -> constr_spec *)
   16.31 -fun constr_spec [] x = raise TERM ("NitpickScope.constr_spec", [Const x])
   16.32 +fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
   16.33    | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
   16.34      case List.find (equal (s, body_type T) o (apsnd body_type o #const))
   16.35                     constrs of
   16.36 @@ -115,7 +115,7 @@
   16.37  (* scope -> typ -> int * int *)
   16.38  fun spec_of_type ({card_assigns, ofs, ...} : scope) T =
   16.39    (card_of_type card_assigns T
   16.40 -   handle TYPE ("NitpickHOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
   16.41 +   handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
   16.42  
   16.43  (* (string -> string) -> scope
   16.44     -> string list * string list * string list * string list * string list *)
   16.45 @@ -205,17 +205,17 @@
   16.46  fun lookup_ints_assign eq asgns key =
   16.47    case triple_lookup eq asgns key of
   16.48      SOME ks => ks
   16.49 -  | NONE => raise ARG ("NitpickScope.lookup_ints_assign", "")
   16.50 +  | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
   16.51  (* theory -> (typ option * int list) list -> typ -> int list *)
   16.52  fun lookup_type_ints_assign thy asgns T =
   16.53    map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T)
   16.54 -  handle ARG ("NitpickScope.lookup_ints_assign", _) =>
   16.55 -         raise TYPE ("NitpickScope.lookup_type_ints_assign", [T], [])
   16.56 +  handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
   16.57 +         raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
   16.58  (* theory -> (styp option * int list) list -> styp -> int list *)
   16.59  fun lookup_const_ints_assign thy asgns x =
   16.60    lookup_ints_assign (const_match thy) asgns x
   16.61 -  handle ARG ("NitpickScope.lookup_ints_assign", _) =>
   16.62 -         raise TERM ("NitpickScope.lookup_const_ints_assign", [Const x])
   16.63 +  handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
   16.64 +         raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x])
   16.65  
   16.66  (* theory -> (styp option * int list) list -> styp -> row option *)
   16.67  fun row_for_constr thy maxes_asgns constr =
   16.68 @@ -315,7 +315,7 @@
   16.69        max < k
   16.70        orelse (forall (not_equal 0) precise_cards andalso doms_card () < k)
   16.71      end
   16.72 -    handle TYPE ("NitpickHOL.card_of_type", _, _) => false
   16.73 +    handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
   16.74  
   16.75  (* theory -> scope_desc -> bool *)
   16.76  fun is_surely_inconsistent_scope_description thy (desc as (card_asgns, _)) =
    17.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Oct 27 12:16:26 2009 +0100
    17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Oct 27 14:40:24 2009 +0100
    17.3 @@ -10,15 +10,14 @@
    17.4    val run_all_tests : unit -> unit
    17.5  end
    17.6  
    17.7 -structure NitpickTests =
    17.8 +structure Nitpick_Tests =
    17.9  struct
   17.10  
   17.11 -open NitpickUtil
   17.12 -open NitpickPeephole
   17.13 -open NitpickRep
   17.14 -open NitpickNut
   17.15 -open NitpickKodkod
   17.16 -open Nitpick
   17.17 +open Nitpick_Util
   17.18 +open Nitpick_Peephole
   17.19 +open Nitpick_Rep
   17.20 +open Nitpick_Nut
   17.21 +open Nitpick_Kodkod
   17.22  
   17.23  val settings =
   17.24    [("solver", "\"zChaff\""),
    18.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Oct 27 12:16:26 2009 +0100
    18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Oct 27 14:40:24 2009 +0100
    18.3 @@ -72,7 +72,7 @@
    18.4    val maybe_quote : string -> string
    18.5  end
    18.6  
    18.7 -structure NitpickUtil : NITPICK_UTIL =
    18.8 +structure Nitpick_Util : NITPICK_UTIL =
    18.9  struct
   18.10  
   18.11  type styp = string * typ
   18.12 @@ -107,7 +107,7 @@
   18.13    | reasonable_power 1 _ = 1
   18.14    | reasonable_power a b =
   18.15      if b < 0 orelse b > max_exponent then
   18.16 -      raise LIMIT ("NitpickUtil.reasonable_power",
   18.17 +      raise LIMIT ("Nitpick_Util.reasonable_power",
   18.18                     "too large exponent (" ^ signed_string_of_int b ^ ")")
   18.19      else
   18.20        let
   18.21 @@ -123,7 +123,7 @@
   18.22      if reasonable_power m r = n then
   18.23        r
   18.24      else
   18.25 -      raise ARG ("NitpickUtil.exact_log",
   18.26 +      raise ARG ("Nitpick_Util.exact_log",
   18.27                   commas (map signed_string_of_int [m, n]))
   18.28    end
   18.29  
   18.30 @@ -133,7 +133,7 @@
   18.31      if reasonable_power r m = n then
   18.32        r
   18.33      else
   18.34 -      raise ARG ("NitpickUtil.exact_root",
   18.35 +      raise ARG ("Nitpick_Util.exact_root",
   18.36                   commas (map signed_string_of_int [m, n]))
   18.37    end
   18.38  
   18.39 @@ -156,7 +156,7 @@
   18.40      fun aux _ [] _ = []
   18.41        | aux i (j :: js) (x :: xs) =
   18.42          if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs
   18.43 -      | aux _ _ _ = raise ARG ("NitpickUtil.filter_indices",
   18.44 +      | aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices",
   18.45                                 "indices unordered or out of range")
   18.46    in aux 0 js xs end
   18.47  fun filter_out_indices js xs =
   18.48 @@ -165,7 +165,7 @@
   18.49      fun aux _ [] xs = xs
   18.50        | aux i (j :: js) (x :: xs) =
   18.51          if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs
   18.52 -      | aux _ _ _ = raise ARG ("NitpickUtil.filter_out_indices",
   18.53 +      | aux _ _ _ = raise ARG ("Nitpick_Util.filter_out_indices",
   18.54                                 "indices unordered or out of range")
   18.55    in aux 0 js xs end
   18.56  
   18.57 @@ -303,5 +303,5 @@
   18.58  
   18.59  end;
   18.60  
   18.61 -structure BasicNitpickUtil : BASIC_NITPICK_UTIL = NitpickUtil;
   18.62 -open BasicNitpickUtil;
   18.63 +structure Basic_Nitpick_Util : BASIC_NITPICK_UTIL = Nitpick_Util;
   18.64 +open Basic_Nitpick_Util;