--- 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;