src/HOL/Tools/Datatype/datatype_case.ML

 Nested case expressions on datatypes.
 *)
 
 signature DATATYPE_CASE =
 sig
+  datatype config = Error | Warning | Quiet;
   val make_case: (string -> DatatypeAux.info option) ->
-    Proof.context -> bool -> string list -> term -> (term * term) list ->
+    Proof.context -> config -> string list -> term -> (term * term) list ->
     term * (term * (int * bool)) list
   val dest_case: (string -> DatatypeAux.info option) -> bool ->
     string list -> term -> (term * (term * term) list) option
   val strip_case: (string -> DatatypeAux.info option) -> bool ->
     term -> (term * (term * term) list) option

     string -> Proof.context -> term list -> term
 end;
 
 structure DatatypeCase : DATATYPE_CASE =
 struct
+
+datatype config = Error | Warning | Quiet;
 
 exception CASE_ERROR of string * int;
 
 fun match_type thy pat ob = Sign.typ_match thy (pat, ob) Vartab.empty;
 

           case_error (quote s ^ " occurs repeatedly in the pattern " ^
             quote (Syntax.string_of_term ctxt pat))
         else x :: xs)
     | _ => I) pat [];
 
-fun gen_make_case ty_match ty_inst type_of tab ctxt err used x clauses =
+fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses =
   let
     fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt
       (Syntax.const "_case1" $ pat $ rhs);
     val _ = map (no_repeat_vars ctxt o fst) clauses;
     val rows = map_index (fn (i, (pat, rhs)) =>

     val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
     val finals = map row_of_pat patts2
     val originals = map (row_of_pat o #2) rows
     val _ = case originals \\ finals of
         [] => ()
-      | is => (if err then case_error else warning)
+        | is => (case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
           ("The following clauses are redundant (covered by preceding clauses):\n" ^
            cat_lines (map (string_of_clause o nth clauses) is));
   in
     (case_tm, patts2)
   end;

             end
         | dest_case1 t = case_error "dest_case1";
       fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
         | dest_case2 t = [t];
       val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
-      val (case_tm, _) = make_case_untyped (tab_of thy) ctxt err []
+      val (case_tm, _) = make_case_untyped (tab_of thy) ctxt
+        (if err then Error else Warning) []
         (fold (fn tT => fn t => Syntax.const "_constrain" $ t $ tT)
            (flat cnstrts) t) cases;
     in case_tm end
   | case_tr _ _ _ ts = case_error "case_tr";