1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Feb 22 10:28:49 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Feb 22 11:57:33 2010 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  exception CTYPE of string * ctype list
     1.5  
     1.6  (* string -> unit *)
     1.7 -fun print_g (s : string) = ()
     1.8 +fun print_g (_ : string) = ()
     1.9  
    1.10  (* var -> string *)
    1.11  val string_for_var = signed_string_of_int
    1.12 @@ -265,7 +265,7 @@
    1.13    end
    1.14  
    1.15  (* cdata -> styp -> ctype *)
    1.16 -fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
    1.17 +fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
    1.18                                  ...}) (x as (_, T)) =
    1.19    if could_exist_alpha_sub_ctype thy alpha_T T then
    1.20      case AList.lookup (op =) (!constr_cache) x of
    1.21 @@ -339,7 +339,7 @@
    1.22       | (S Minus, S Plus) => NONE
    1.23       | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
    1.24       | _ => do_sign_atom_comp Eq [] a1 a2 accum)
    1.25 -  | do_sign_atom_comp cmp xs a1 a2 (accum as (lits, comps)) =
    1.26 +  | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
    1.27      SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
    1.28  
    1.29  (* comp -> var list -> ctype -> ctype -> (literal list * comp list) option
    1.30 @@ -367,7 +367,7 @@
    1.31      (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
    1.32       handle Library.UnequalLengths =>
    1.33              raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
    1.34 -  | do_ctype_comp cmp xs (CType _) (CType _) accum =
    1.35 +  | do_ctype_comp _ _ (CType _) (CType _) accum =
    1.36      accum (* no need to compare them thanks to the cache *)
    1.37    | do_ctype_comp _ _ C1 C2 _ =
    1.38      raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
    1.39 @@ -435,13 +435,6 @@
    1.40  val add_ctype_is_right_unique = add_notin_ctype_fv Minus
    1.41  val add_ctype_is_right_total = add_notin_ctype_fv Plus
    1.42  
    1.43 -(* constraint_set -> constraint_set -> constraint_set *)
    1.44 -fun unite (CSet (lits1, comps1, sexps1)) (CSet (lits2, comps2, sexps2)) =
    1.45 -    (case SOME lits1 |> fold do_literal lits2 of
    1.46 -       NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
    1.47 -     | SOME lits => CSet (lits, comps1 @ comps2, sexps1 @ sexps2))
    1.48 -  | unite _ _ = UnsolvableCSet
    1.49 -
    1.50  (* sign -> bool *)
    1.51  fun bool_from_sign Plus = false
    1.52    | bool_from_sign Minus = true
    1.53 @@ -480,10 +473,6 @@
    1.54               SOME b => (x, sign_from_bool b) :: accum
    1.55             | NONE => accum) (max_var downto 1) lits
    1.56  
    1.57 -(* literal list -> sign_atom -> sign option *)
    1.58 -fun lookup_sign_atom _ (S sn) = SOME sn
    1.59 -  | lookup_sign_atom lit (V x) = AList.lookup (op =) lit x
    1.60 -
    1.61  (* comp -> string *)
    1.62  fun string_for_comp (a1, a2, cmp, xs) =
    1.63    string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^
    1.64 @@ -522,9 +511,6 @@
    1.65        | _ => NONE
    1.66      end
    1.67  
    1.68 -(* var -> constraint_set -> bool *)
    1.69 -val is_solvable = is_some oo solve
    1.70 -
    1.71  type ctype_schema = ctype * constraint_set
    1.72  type ctype_context =
    1.73    {bounds: ctype list,
    1.74 @@ -545,8 +531,8 @@
    1.75    handle List.Empty => initial_gamma
    1.76  
    1.77  (* cdata -> term -> accumulator -> ctype * accumulator *)
    1.78 -fun consider_term (cdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
    1.79 -                                          def_table, ...},
    1.80 +fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
    1.81 +                                         def_table, ...},
    1.82                               alpha_T, max_fresh, ...}) =
    1.83    let
    1.84      (* typ -> ctype *)
    1.85 @@ -765,7 +751,7 @@
    1.86           | Var _ => (print_g "*** Var"; unsolvable)
    1.87           | Bound j => (nth bounds j, accum)
    1.88           | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum)
    1.89 -         | Abs (s, T, t') =>
    1.90 +         | Abs (_, T, t') =>
    1.91             ((case t' of
    1.92                 t1' $ Bound 0 =>
    1.93                 if not (loose_bvar1 (t1', 0)) then
    1.94 @@ -806,7 +792,7 @@
    1.95    in do_term end
    1.96  
    1.97  (* cdata -> sign -> term -> accumulator -> accumulator *)
    1.98 -fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
    1.99 +fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) =
   1.100    let
   1.101      (* typ -> ctype *)
   1.102      val ctype_for = fresh_ctype_for_type cdata
   1.103 @@ -814,7 +800,7 @@
   1.104      val do_term = consider_term cdata
   1.105      (* sign -> term -> accumulator -> accumulator *)
   1.106      fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
   1.107 -      | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
   1.108 +      | do_formula sn t (accum as (gamma, cset)) =
   1.109          let
   1.110            (* term -> accumulator -> accumulator *)
   1.111            val do_co_formula = do_formula sn