1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 12:16:26 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 14:40:24 2009 +0100
     1.3 @@ -62,15 +62,15 @@
     1.4  structure Nitpick : NITPICK =
     1.5  struct
     1.6  
     1.7 -open NitpickUtil
     1.8 -open NitpickHOL
     1.9 -open NitpickMono
    1.10 -open NitpickScope
    1.11 -open NitpickPeephole
    1.12 -open NitpickRep
    1.13 -open NitpickNut
    1.14 -open NitpickKodkod
    1.15 -open NitpickModel
    1.16 +open Nitpick_Util
    1.17 +open Nitpick_HOL
    1.18 +open Nitpick_Mono
    1.19 +open Nitpick_Scope
    1.20 +open Nitpick_Peephole
    1.21 +open Nitpick_Rep
    1.22 +open Nitpick_Nut
    1.23 +open Nitpick_Kodkod
    1.24 +open Nitpick_Model
    1.25  
    1.26  type params = {
    1.27    cards_assigns: (typ option * int list) list,
    1.28 @@ -355,21 +355,21 @@
    1.29      val effective_sat_solver =
    1.30        if sat_solver <> "smart" then
    1.31          if need_incremental andalso
    1.32 -           not (sat_solver mem KodkodSAT.configured_sat_solvers true) then
    1.33 +           not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then
    1.34            (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
    1.35                         \be used instead of " ^ quote sat_solver ^ "."));
    1.36             "SAT4J")
    1.37          else
    1.38            sat_solver
    1.39        else
    1.40 -        KodkodSAT.smart_sat_solver_name need_incremental
    1.41 +        Kodkod_SAT.smart_sat_solver_name need_incremental
    1.42      val _ =
    1.43        if sat_solver = "smart" then
    1.44          print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^
    1.45                            ". The following" ^
    1.46                            (if need_incremental then " incremental " else " ") ^
    1.47                            "solvers are configured: " ^
    1.48 -                          commas (map quote (KodkodSAT.configured_sat_solvers
    1.49 +                          commas (map quote (Kodkod_SAT.configured_sat_solvers
    1.50                                                         need_incremental)) ^ ".")
    1.51        else
    1.52          ()
    1.53 @@ -439,7 +439,7 @@
    1.54          val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
    1.55          val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
    1.56                        PrintMode.setmp [] multiline_string_for_scope scope
    1.57 -        val kodkod_sat_solver = KodkodSAT.sat_solver_spec effective_sat_solver
    1.58 +        val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver
    1.59                                  |> snd
    1.60          val delay = if liberal then
    1.61                        Option.map (fn time => Time.- (time, Time.now ()))
    1.62 @@ -483,7 +483,7 @@
    1.63                 defs = nondef_fs @ def_fs @ declarative_axioms})
    1.64        end
    1.65        handle LIMIT (loc, msg) =>
    1.66 -             if loc = "NitpickKodkod.check_arity"
    1.67 +             if loc = "Nitpick_Kodkod.check_arity"
    1.68                  andalso not (Typtab.is_empty ofs) then
    1.69                 problem_for_scope liberal
    1.70                     {ext_ctxt = ext_ctxt, card_assigns = card_assigns,