# HG changeset patch
# User wenzelm
# Date 1374089127 -7200
# Node ID 2fa3110539a50cd908d456a123057724c0fecc73
# Parent  6419ada0664acb3897c715f03106e2d5a6745bd9
more opportunistic string_of_clause, to make double-sure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);

diff -r 6419ada0664a -r 2fa3110539a5 src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Wed Jul 17 21:04:38 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Jul 17 21:25:27 2013 +0200
@@ -366,7 +366,12 @@
 fun make_case ctxt config used x clauses =
   let
     fun string_of_clause (pat, rhs) =
-      Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
+      (case try (fn () => (* FIXME may crash!? *)
+        Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs)) ()
+       of
+        SOME s => s
+      | NONE => Markup.markup Markup.intensify "<malformed>");
+
     val _ = map (no_repeat_vars ctxt o fst) clauses;
     val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;
     val rangeT =
@@ -386,7 +391,7 @@
       | is =>
           if config = Quiet then ()
           else
-            (if config = Error then case_error else warning)
+            (if config = Error then case_error else warning (*FIXME lack of syntactic context!?*))
               ("The following clauses are redundant (covered by preceding clauses):\n" ^
                 cat_lines (map (string_of_clause o nth clauses) is)));
   in