# HG changeset patch
# User bulwahn
# Date 1253715612 -7200
# Node ID fbd2248507676b5f43b989afabecfa9ae570e019
# Parent  cc0bae788b7eb70f0f7ad9440117d01a441f7196
adapted configuration for DatatypeCase.make_case

diff -r cc0bae788b7e -r fbd224850767 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -26,7 +26,7 @@
   val info_of_case : theory -> string -> info option
   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
   val distinct_simproc : simproc
-  val make_case :  Proof.context -> bool -> string list -> term ->
+  val make_case :  Proof.context -> DatatypeCase.config -> string list -> term ->
     (term * term) list -> term * (term * (int * bool)) list
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
   val read_typ: theory ->
diff -r cc0bae788b7e -r fbd224850767 src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -7,8 +7,9 @@
 
 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
@@ -23,6 +24,8 @@
 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;
@@ -260,7 +263,7 @@
         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);
@@ -285,7 +288,7 @@
     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
@@ -338,7 +341,8 @@
       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
diff -r cc0bae788b7e -r fbd224850767 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -1179,7 +1179,7 @@
     val v' = Free (name', T);
   in
     lambda v (fst (Datatype.make_case
-      (ProofContext.init thy) false [] v
+      (ProofContext.init thy) DatatypeCase.Quiet [] v
       [(mk_tuple out_ts,
         if null eqs'' then success_t
         else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $