1.1 --- a/src/HOL/Tools/case_translation.ML	Wed Jul 17 21:04:38 2013 +0200
     1.2 +++ b/src/HOL/Tools/case_translation.ML	Wed Jul 17 21:25:27 2013 +0200
     1.3 @@ -366,7 +366,12 @@
     1.4  fun make_case ctxt config used x clauses =
     1.5    let
     1.6      fun string_of_clause (pat, rhs) =
     1.7 -      Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
     1.8 +      (case try (fn () => (* FIXME may crash!? *)
     1.9 +        Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs)) ()
    1.10 +       of
    1.11 +        SOME s => s
    1.12 +      | NONE => Markup.markup Markup.intensify "<malformed>");
    1.13 +
    1.14      val _ = map (no_repeat_vars ctxt o fst) clauses;
    1.15      val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;
    1.16      val rangeT =
    1.17 @@ -386,7 +391,7 @@
    1.18        | is =>
    1.19            if config = Quiet then ()
    1.20            else
    1.21 -            (if config = Error then case_error else warning)
    1.22 +            (if config = Error then case_error else warning (*FIXME lack of syntactic context!?*))
    1.23                ("The following clauses are redundant (covered by preceding clauses):\n" ^
    1.24                  cat_lines (map (string_of_clause o nth clauses) is)));
    1.25    in