1.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Oct 27 12:16:26 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Oct 27 14:40:24 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature NITPICK_SCOPE =
     1.6  sig
     1.7 -  type extended_context = NitpickHOL.extended_context
     1.8 +  type extended_context = Nitpick_HOL.extended_context
     1.9  
    1.10    type constr_spec = {
    1.11      const: styp,
    1.12 @@ -47,11 +47,11 @@
    1.13      -> int list -> typ list -> typ list -> scope list
    1.14  end;
    1.15  
    1.16 -structure NitpickScope : NITPICK_SCOPE =
    1.17 +structure Nitpick_Scope : NITPICK_SCOPE =
    1.18  struct
    1.19  
    1.20 -open NitpickUtil
    1.21 -open NitpickHOL
    1.22 +open Nitpick_Util
    1.23 +open Nitpick_HOL
    1.24  
    1.25  type constr_spec = {
    1.26    const: styp,
    1.27 @@ -85,7 +85,7 @@
    1.28    List.find (equal T o #typ) dtypes
    1.29  
    1.30  (* dtype_spec list -> styp -> constr_spec *)
    1.31 -fun constr_spec [] x = raise TERM ("NitpickScope.constr_spec", [Const x])
    1.32 +fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
    1.33    | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
    1.34      case List.find (equal (s, body_type T) o (apsnd body_type o #const))
    1.35                     constrs of
    1.36 @@ -115,7 +115,7 @@
    1.37  (* scope -> typ -> int * int *)
    1.38  fun spec_of_type ({card_assigns, ofs, ...} : scope) T =
    1.39    (card_of_type card_assigns T
    1.40 -   handle TYPE ("NitpickHOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
    1.41 +   handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
    1.42  
    1.43  (* (string -> string) -> scope
    1.44     -> string list * string list * string list * string list * string list *)
    1.45 @@ -205,17 +205,17 @@
    1.46  fun lookup_ints_assign eq asgns key =
    1.47    case triple_lookup eq asgns key of
    1.48      SOME ks => ks
    1.49 -  | NONE => raise ARG ("NitpickScope.lookup_ints_assign", "")
    1.50 +  | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
    1.51  (* theory -> (typ option * int list) list -> typ -> int list *)
    1.52  fun lookup_type_ints_assign thy asgns T =
    1.53    map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T)
    1.54 -  handle ARG ("NitpickScope.lookup_ints_assign", _) =>
    1.55 -         raise TYPE ("NitpickScope.lookup_type_ints_assign", [T], [])
    1.56 +  handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
    1.57 +         raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
    1.58  (* theory -> (styp option * int list) list -> styp -> int list *)
    1.59  fun lookup_const_ints_assign thy asgns x =
    1.60    lookup_ints_assign (const_match thy) asgns x
    1.61 -  handle ARG ("NitpickScope.lookup_ints_assign", _) =>
    1.62 -         raise TERM ("NitpickScope.lookup_const_ints_assign", [Const x])
    1.63 +  handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
    1.64 +         raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x])
    1.65  
    1.66  (* theory -> (styp option * int list) list -> styp -> row option *)
    1.67  fun row_for_constr thy maxes_asgns constr =
    1.68 @@ -315,7 +315,7 @@
    1.69        max < k
    1.70        orelse (forall (not_equal 0) precise_cards andalso doms_card () < k)
    1.71      end
    1.72 -    handle TYPE ("NitpickHOL.card_of_type", _, _) => false
    1.73 +    handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
    1.74  
    1.75  (* theory -> scope_desc -> bool *)
    1.76  fun is_surely_inconsistent_scope_description thy (desc as (card_asgns, _)) =