1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Oct 27 12:16:26 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Oct 27 14:40:24 2009 +0100
     1.3 @@ -7,17 +7,17 @@
     1.4  
     1.5  signature NITPICK_MONO =
     1.6  sig
     1.7 -  type extended_context = NitpickHOL.extended_context
     1.8 +  type extended_context = Nitpick_HOL.extended_context
     1.9  
    1.10    val formulas_monotonic :
    1.11      extended_context -> typ -> term list -> term list -> term -> bool
    1.12  end;
    1.13  
    1.14 -structure NitpickMono : NITPICK_MONO =
    1.15 +structure Nitpick_Mono : NITPICK_MONO =
    1.16  struct
    1.17  
    1.18 -open NitpickUtil
    1.19 -open NitpickHOL
    1.20 +open Nitpick_Util
    1.21 +open Nitpick_HOL
    1.22  
    1.23  type var = int
    1.24  
    1.25 @@ -363,11 +363,11 @@
    1.26                    accum =
    1.27      (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
    1.28       handle Library.UnequalLengths =>
    1.29 -            raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2]))
    1.30 +            raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
    1.31    | do_ctype_comp cmp xs (CType _) (CType _) accum =
    1.32      accum (* no need to compare them thanks to the cache *)
    1.33    | do_ctype_comp _ _ C1 C2 _ =
    1.34 -    raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2])
    1.35 +    raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
    1.36  
    1.37  (* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *)
    1.38  fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
    1.39 @@ -413,7 +413,7 @@
    1.40    | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
    1.41      accum |> fold (do_notin_ctype_fv sn sexp) Cs
    1.42    | do_notin_ctype_fv _ _ C _ =
    1.43 -    raise CTYPE ("NitpickMono.do_notin_ctype_fv", [C])
    1.44 +    raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C])
    1.45  
    1.46  (* sign -> ctype -> constraint_set -> constraint_set *)
    1.47  fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
    1.48 @@ -584,13 +584,13 @@
    1.49        case ctype_for (nth_range_type 2 T) of
    1.50          C as CPair (a_C, b_C) =>
    1.51          (CFun (a_C, S Neg, CFun (b_C, S Neg, C)), accum)
    1.52 -      | C => raise CTYPE ("NitpickMono.consider_term.do_pair_constr", [C])
    1.53 +      | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
    1.54      (* int -> typ -> accumulator -> ctype * accumulator *)
    1.55      fun do_nth_pair_sel n T =
    1.56        case ctype_for (domain_type T) of
    1.57          C as CPair (a_C, b_C) =>
    1.58          pair (CFun (C, S Neg, if n = 0 then a_C else b_C))
    1.59 -      | C => raise CTYPE ("NitpickMono.consider_term.do_nth_pair_sel", [C])
    1.60 +      | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
    1.61      val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
    1.62      (* typ -> term -> accumulator -> ctype * accumulator *)
    1.63      fun do_bounded_quantifier abs_T bound_t body_t accum =
    1.64 @@ -770,7 +770,7 @@
    1.65               | _ => case C1 of
    1.66                        CFun (C11, _, C12) =>
    1.67                        (C12, accum ||> add_is_sub_ctype C2 C11)
    1.68 -                    | _ => raise CTYPE ("NitpickMono.consider_term.do_term \
    1.69 +                    | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \
    1.70                                          \(op $)", [C1])
    1.71             end)
    1.72          |> tap (fn (C, _) =>
    1.73 @@ -906,7 +906,7 @@
    1.74            | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum
    1.75            | @{const "op &"} $ t1 $ t2 => accum |> do_formula t1 |> do_formula t2
    1.76            | @{const "op -->"} $ t1 $ t2 => do_implies t1 t2 accum
    1.77 -          | _ => raise TERM ("NitpickMono.consider_definitional_axiom.\
    1.78 +          | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
    1.79                               \do_formula", [t])
    1.80      in do_formula t end
    1.81