# HG changeset patch
# User wenzelm
# Date 1374064413 -7200
# Node ID 554d684d8520380537847449ac62d5f72cc3f795
# Parent  8d749ebd9ab8c2412cbf0c0e12f89b796cb2c051
non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);

diff -r 8d749ebd9ab8 -r 554d684d8520 src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Wed Jul 17 13:45:55 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Jul 17 14:33:33 2013 +0200
@@ -384,9 +384,11 @@
       (case subtract (op =) tags (map (snd o snd) rows) of
         [] => ()
       | 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)));
+          if config = Quiet then ()
+          else
+            (if config = Error then case_error else warning)
+              ("The following clauses are redundant (covered by preceding clauses):\n" ^
+                cat_lines (map (string_of_clause o nth clauses) is)));
   in
     case_tm
   end;