1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Apr 23 19:16:52 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Apr 23 19:18:39 2010 +0200
     1.3 @@ -348,7 +348,7 @@
     1.4      fun monotonicity_message Ts extra =
     1.5        let val ss = map (quote o string_for_type ctxt) Ts in
     1.6          "The type" ^ plural_s_for_list ss ^ " " ^
     1.7 -        space_implode " " (Sledgehammer_Util.serial_commas "and" ss) ^ " " ^
     1.8 +        space_implode " " (serial_commas "and" ss) ^ " " ^
     1.9          (if none_true monos then
    1.10             "passed the monotonicity test"
    1.11           else
    1.12 @@ -686,8 +686,7 @@
    1.13                          options
    1.14                  in
    1.15                    print ("Try again with " ^
    1.16 -                         space_implode " "
    1.17 -                             (Sledgehammer_Util.serial_commas "and" ss) ^
    1.18 +                         space_implode " " (serial_commas "and" ss) ^
    1.19                           " to confirm that the " ^ das_wort_model ^
    1.20                           " is genuine.")
    1.21                  end

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Apr 23 19:16:52 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Apr 23 19:18:39 2010 +0200
     2.3 @@ -217,7 +217,6 @@
     2.4  structure Nitpick_HOL : NITPICK_HOL =
     2.5  struct
     2.6  
     2.7 -open Sledgehammer_Util
     2.8  open Nitpick_Util
     2.9  
    2.10  type const_table = term list Symtab.table

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Apr 23 19:16:52 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Apr 23 19:18:39 2010 +0200
     3.3 @@ -176,7 +176,7 @@
     3.4      (* bool -> bool option -> string -> bool option *)
     3.5      fun general_lookup_bool option default_value name =
     3.6        case lookup name of
     3.7 -        SOME s => Sledgehammer_Util.parse_bool_option option name s
     3.8 +        SOME s => parse_bool_option option name s
     3.9        | NONE => default_value
    3.10      (* string -> bool *)
    3.11      val lookup_bool = the o general_lookup_bool false (SOME false)
    3.12 @@ -235,8 +235,7 @@
    3.13        :: map (fn (name, value) =>
    3.14                   (SOME (read (String.extract (name, size prefix + 1, NONE))),
    3.15                    value |> stringify_raw_param_value
    3.16 -                        |> Sledgehammer_Util.parse_bool_option false name
    3.17 -                        |> the))
    3.18 +                        |> parse_bool_option false name |> the))
    3.19               (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
    3.20      (* (string -> 'a) -> string -> ('a option * bool option) list *)
    3.21      fun lookup_bool_option_assigns read prefix =
    3.22 @@ -244,13 +243,13 @@
    3.23        :: map (fn (name, value) =>
    3.24                   (SOME (read (String.extract (name, size prefix + 1, NONE))),
    3.25                    value |> stringify_raw_param_value
    3.26 -                        |> Sledgehammer_Util.parse_bool_option true name))
    3.27 +                        |> parse_bool_option true name))
    3.28               (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
    3.29      (* string -> Time.time option *)
    3.30      fun lookup_time name =
    3.31        case lookup name of
    3.32          NONE => NONE
    3.33 -      | SOME s => Sledgehammer_Util.parse_time_option name s
    3.34 +      | SOME s => parse_time_option name s
    3.35      (* string -> term list *)
    3.36      val lookup_term_list =
    3.37        AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Apr 23 19:16:52 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Apr 23 19:18:39 2010 +0200
     4.3 @@ -194,11 +194,8 @@
     4.4                else
     4.5                  [])
     4.6    in
     4.7 -    if null ss then
     4.8 -      []
     4.9 -    else
    4.10 -      Sledgehammer_Util.serial_commas "and" ss
    4.11 -      |> map Pretty.str |> Pretty.breaks
    4.12 +    if null ss then []
    4.13 +    else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks
    4.14    end
    4.15  
    4.16  (* scope -> string *)

     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Apr 23 19:16:52 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Apr 23 19:18:39 2010 +0200
     5.3 @@ -48,6 +48,10 @@
     5.4    val is_substring_of : string -> string -> bool
     5.5    val plural_s : int -> string
     5.6    val plural_s_for_list : 'a list -> string
     5.7 +  val serial_commas : string -> string list -> string list
     5.8 +  val timestamp : unit -> string
     5.9 +  val parse_bool_option : bool -> string -> string -> bool option
    5.10 +  val parse_time_option : string -> string -> Time.time option
    5.11    val flip_polarity : polarity -> polarity
    5.12    val prop_T : typ
    5.13    val bool_T : typ
    5.14 @@ -61,6 +65,8 @@
    5.15    val pstrs : string -> Pretty.T list
    5.16    val unyxml : string -> string
    5.17    val maybe_quote : string -> string
    5.18 +  val hashw : word * word -> word
    5.19 +  val hashw_string : string * word -> word
    5.20  end;
    5.21  
    5.22  structure Nitpick_Util : NITPICK_UTIL =
    5.23 @@ -82,7 +88,6 @@
    5.24  (* ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd *)
    5.25  fun curry3 f = fn x => fn y => fn z => f (x, y, z)
    5.26  
    5.27 -(* ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c *)
    5.28  fun pairf f g x = (f x, g x)
    5.29  
    5.30  (* (bool -> 'a) -> 'a * 'a *)
    5.31 @@ -233,10 +238,20 @@
    5.32                                                    (Substring.full stack))))
    5.33  
    5.34  (* int -> string *)
    5.35 -fun plural_s n = if n = 1 then "" else "s"
    5.36 +val plural_s = Sledgehammer_Util.plural_s
    5.37  (* 'a list -> string *)
    5.38  fun plural_s_for_list xs = plural_s (length xs)
    5.39  
    5.40 +(* string -> string list -> string list *)
    5.41 +val serial_commas = Sledgehammer_Util.serial_commas
    5.42 +
    5.43 +(* unit -> string *)
    5.44 +val timestamp = Sledgehammer_Util.timestamp
    5.45 +(* bool -> string -> string -> bool option *)
    5.46 +val parse_bool_option = Sledgehammer_Util.parse_bool_option
    5.47 +(* string -> string -> Time.time option *)
    5.48 +val parse_time_option = Sledgehammer_Util.parse_time_option
    5.49 +
    5.50  (* polarity -> polarity *)
    5.51  fun flip_polarity Pos = Neg
    5.52    | flip_polarity Neg = Pos
    5.53 @@ -290,4 +305,14 @@
    5.54             OuterKeyword.is_keyword s) ? quote
    5.55    end
    5.56  
    5.57 +(* This hash function is recommended in Compilers: Principles, Techniques, and
    5.58 +   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
    5.59 +   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
    5.60 +(* word * word -> word *)
    5.61 +fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
    5.62 +(* Char.char * word -> word *)
    5.63 +fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
    5.64 +(* string * word -> word *)
    5.65 +fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
    5.66 +
    5.67  end;